coqdomain.py 文件源码

def add_coqtop_output(self):
        """Add coqtop's responses to a Sphinx AST

        Finds nodes to process using is_coqtop_block."""
        with CoqTop(color=True) as repl:
            for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block):
                options = node['coqtop_options']
                opt_undo, opt_reset, opt_input, opt_output = self.parse_options(options)

                if opt_reset:
                    repl.sendone("Reset Initial.")
                pairs = []
                for sentence in self.split_sentences(node.rawsource):
                    pairs.append((sentence, repl.sendone(sentence)))
                if opt_undo:
                    repl.sendone("Undo {}.".format(len(pairs)))

                dli = nodes.definition_list_item()
                for sentence, output in pairs:
                    # Use Coqdoq to highlight input
                    in_chunks = highlight_using_coqdoc(sentence)
                    dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input))
                    # Parse ANSI sequences to highlight output
                    out_chunks = AnsiColorsParser().colorize_str(output)
                    dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output))
                node.clear()
                node.rawsource = self.make_rawsource(pairs, opt_input, opt_output)
                node['classes'].extend(self.block_classes(opt_input or opt_output))
                node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset)
                node += nodes.definition_list(node.rawsource, dli)