diff options
Diffstat (limited to 'doc/tools/coqrst/notations/sphinx.py')
| -rw-r--r-- | doc/tools/coqrst/notations/sphinx.py | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index 889bf70a4..26a5f6968 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -20,6 +20,8 @@ from .TacticNotationsVisitor import TacticNotationsVisitor from docutils import nodes from sphinx import addnodes +import sys + class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): def defaultResult(self): return [] @@ -62,6 +64,12 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): node = nodes.inline(hole, token_name, classes=["hole"]) 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 + return [nodes.inline(metachar, token_name, classes=["meta"])] + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): return [nodes.Text(" ")] |