diff options
Diffstat (limited to 'doc/tools/coqrst/notations/html.py')
| -rw-r--r-- | doc/tools/coqrst/notations/html.py | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index 44212d788..87a41cf9f 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -41,9 +41,16 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): 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): - tags.span(ctx.METACHAR().getText()[1:], _class="meta") + 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 |