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])
评论列表
文章目录