lean_sphinx.py 文件源码

python
阅读 32 收藏 0 点赞 0 评论 0

项目:reference 作者: leanprover 项目源码 文件源码
def process_lean_nodes(app, doctree, fromdocname):
    for node in doctree.traverse(nodes.literal_block):
        if node['language'] != 'lean': continue

        new_node = lean_code_goodies()
        new_node['full_code'] = node.rawsource
        node.replace_self([new_node])

        code = node.rawsource
        m = re.search(r'--[^\n]*BEGIN[^\n]*\n(.*)--[^\n]*END', code, re.DOTALL)
        if m:
            node = nodes.literal_block(m.group(1), m.group(1))
            node['language'] = 'lean'
        new_node += node

        if app.builder.name.startswith('epub'):
            new_node.replace_self([node])
评论列表
文章目录


问题


面经


文章

微信
公众号

扫码关注公众号