diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /doc/tools/coqrst/notations/html.py | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'doc/tools/coqrst/notations/html.py')
-rw-r--r-- | doc/tools/coqrst/notations/html.py | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py new file mode 100644 index 00000000..87a41cf9 --- /dev/null +++ b/doc/tools/coqrst/notations/html.py @@ -0,0 +1,75 @@ +########################################################################## +## # 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 raw HTML. + +Uses the dominate package. +""" + +from dominate import tags + +from .parsing import parse +from .TacticNotationsParser import TacticNotationsParser +from .TacticNotationsVisitor import TacticNotationsVisitor + +class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): + with tags.span(_class="repeat-wrapper"): + with tags.span(_class="repeat"): + self.visitChildren(ctx) + repeat_marker = ctx.LGROUP().getText()[1] + separator = ctx.ATOM() + tags.sup(repeat_marker) + if separator: + tags.sub(separator.getText()) + + def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext): + sp = tags.span(_class="curlies") + sp.add("{") + with sp: + self.visitChildren(ctx) + sp.add("}") + + def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): + tags.span(ctx.ATOM().getText()) + + def visitHole(self, ctx:TacticNotationsParser.HoleContext): + tags.span(ctx.ID().getText()[1:], _class="hole") + sub = ctx.SUB() + if sub: + tags.sub(sub.getText()[1:]) + + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + txt = ctx.METACHAR().getText()[1:] + if (txt == "{") or (txt == "}"): + tags.span(txt) + else: + tags.span(txt, _class="meta") + + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): + tags.span(" ") # TODO: no need for a <span> here + +def htmlize(notation): + """Translate notation to a dominate HTML tree""" + top = tags.span(_class='notation') + with top: + TacticNotationsToHTMLVisitor().visit(parse(notation)) + return top + +def htmlize_str(notation): + """Translate notation to a raw HTML document""" + # ‘pretty=True’ introduces spurious spaces + return htmlize(notation).render(pretty=False) + +def htmlize_p(notation): + """Like `htmlize`, wrapped in a ‘p’. + Does not return: instead, must be run in a dominate context. + """ + with tags.p(): + htmlize(notation) |