diff options
Diffstat (limited to 'doc/tools/coqrst/notations/sphinx.py')
-rw-r--r-- | doc/tools/coqrst/notations/sphinx.py | 102 |
1 files changed, 102 insertions, 0 deletions
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py new file mode 100644 index 00000000..e05b8341 --- /dev/null +++ b/doc/tools/coqrst/notations/sphinx.py @@ -0,0 +1,102 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## +"""A visitor for ANTLR notation ASTs, producing Sphinx nodes. + +Unlike the HTML visitor, this produces Sphinx-friendly nodes that can be used by +all backends. If you just want HTML output, use the HTML visitor. +""" + +from .parsing import parse +from .TacticNotationsParser import TacticNotationsParser +from .TacticNotationsVisitor import TacticNotationsVisitor + +from docutils import nodes +from sphinx import addnodes + +import sys + +class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): + def defaultResult(self): + return [] + + def aggregateResult(self, aggregate, nextResult): + if nextResult: + aggregate.extend(nextResult) + return aggregate + + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): + # Uses inline nodes instead of subscript and superscript to ensure that + # we get the right customization hooks at the LaTeX level + wrapper = nodes.inline('', '', classes=['repeat-wrapper']) + wrapper += nodes.inline('', '', *self.visitChildren(ctx), classes=["repeat"]) + + repeat_marker = ctx.LGROUP().getText()[1] + wrapper += nodes.inline(repeat_marker, repeat_marker, classes=['notation-sup']) + + separator = ctx.ATOM() + if separator: + sep = separator.getText() + wrapper += nodes.inline(sep, sep, classes=['notation-sub']) + + return [wrapper] + + def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext): + sp = nodes.inline('', '', classes=["curlies"]) + sp += nodes.Text("{") + sp.extend(self.visitChildren(ctx)) + sp += nodes.Text("}") + return [sp] + + def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): + atom = ctx.ATOM().getText() + sub = ctx.SUB() + node = nodes.inline(atom, atom) + + if sub: + sub_index = sub.getText()[2:] + node += nodes.subscript(sub_index, sub_index) + + return [node] + + def visitHole(self, ctx:TacticNotationsParser.HoleContext): + hole = ctx.ID().getText() + token_name = hole[1:] + node = nodes.inline(hole, token_name, classes=["hole"]) + + sub = ctx.SUB() + if sub: + sub_index = sub.getText()[2:] + node += nodes.subscript(sub_index, sub_index) + + return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)] + + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + meta = ctx.METACHAR().getText() + metachar = meta[1:] # remove escape char + token_name = metachar + if (metachar == "{") or (metachar == "}"): + classes=[] + else: + classes=["meta"] + return [nodes.inline(metachar, token_name, classes=classes)] + + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): + return [nodes.Text(" ")] + +def sphinxify(notation): + """Translate notation into a Sphinx document tree""" + vs = TacticNotationsToSphinxVisitor() + return vs.visit(parse(notation)) + +def main(): + print(sphinxify("a := {+, b {+ c}}")) + +if __name__ == '__main__': + main() |