diff options
Diffstat (limited to 'doc/tools/coqrst/notations/html.py')
| -rw-r--r-- | doc/tools/coqrst/notations/html.py | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index 44212d788..9c94a4b2d 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -43,7 +43,11 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): tags.span(ctx.ID().getText()[1:], _class="hole") 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 |