[Sphinx] Make it possible to espace { by %{ in custom grammars

3 files changed, 19 insertions, 15 deletions

diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g
index 5176c51d2..68658fe49 100644
--- a/doc/tools/coqrst/notations/TacticNotations.g
+++ b/doc/tools/coqrst/notations/TacticNotations.g
@@ -26,7 +26,7 @@ hole: ID;
 LGROUP: '{' [+*?];
 LBRACE: '{';
 RBRACE: '}';
-METACHAR: '%' [|()];
+METACHAR: '%' [|(){}];
 ATOM: '@' | ~[@{} ]+;
 ID: '@' [a-zA-Z0-9_]+;
 WHITESPACE: ' '+;
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py
index ffa774b9b..61d8d2f9e 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.py
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py
@@ -12,19 +12,19 @@ def serializedATN():
         buf.write("\4\b\t\b\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3\5\3\6\3")
         buf.write("\6\6\6\36\n\6\r\6\16\6\37\5\6\"\n\6\3\7\3\7\6\7&\n\7\r")
         buf.write("\7\16\7\'\3\b\6\b+\n\b\r\b\16\b,\2\2\t\3\3\5\4\7\5\t\6")
-        buf.write("\13\7\r\b\17\t\3\2\6\4\2,-AA\4\2*+~~\6\2\"\"BB}}\177\177")
-        buf.write("\6\2\62;C\\aac|\2\61\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2")
-        buf.write("\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\3")
-        buf.write("\21\3\2\2\2\5\24\3\2\2\2\7\26\3\2\2\2\t\30\3\2\2\2\13")
-        buf.write("!\3\2\2\2\r#\3\2\2\2\17*\3\2\2\2\21\22\7}\2\2\22\23\t")
-        buf.write("\2\2\2\23\4\3\2\2\2\24\25\7}\2\2\25\6\3\2\2\2\26\27\7")
-        buf.write("\177\2\2\27\b\3\2\2\2\30\31\7\'\2\2\31\32\t\3\2\2\32\n")
-        buf.write("\3\2\2\2\33\"\7B\2\2\34\36\n\4\2\2\35\34\3\2\2\2\36\37")
-        buf.write("\3\2\2\2\37\35\3\2\2\2\37 \3\2\2\2 \"\3\2\2\2!\33\3\2")
-        buf.write("\2\2!\35\3\2\2\2\"\f\3\2\2\2#%\7B\2\2$&\t\5\2\2%$\3\2")
-        buf.write("\2\2&\'\3\2\2\2\'%\3\2\2\2\'(\3\2\2\2(\16\3\2\2\2)+\7")
-        buf.write("\"\2\2*)\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\20\3\2")
-        buf.write("\2\2\7\2\37!\',\2")
+        buf.write("\13\7\r\b\17\t\3\2\6\4\2,-AA\4\2*+}\177\6\2\"\"BB}}\177")
+        buf.write("\177\6\2\62;C\\aac|\2\61\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3")
+        buf.write("\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2")
+        buf.write("\2\3\21\3\2\2\2\5\24\3\2\2\2\7\26\3\2\2\2\t\30\3\2\2\2")
+        buf.write("\13!\3\2\2\2\r#\3\2\2\2\17*\3\2\2\2\21\22\7}\2\2\22\23")
+        buf.write("\t\2\2\2\23\4\3\2\2\2\24\25\7}\2\2\25\6\3\2\2\2\26\27")
+        buf.write("\7\177\2\2\27\b\3\2\2\2\30\31\7\'\2\2\31\32\t\3\2\2\32")
+        buf.write("\n\3\2\2\2\33\"\7B\2\2\34\36\n\4\2\2\35\34\3\2\2\2\36")
+        buf.write("\37\3\2\2\2\37\35\3\2\2\2\37 \3\2\2\2 \"\3\2\2\2!\33\3")
+        buf.write("\2\2\2!\35\3\2\2\2\"\f\3\2\2\2#%\7B\2\2$&\t\5\2\2%$\3")
+        buf.write("\2\2\2&\'\3\2\2\2\'%\3\2\2\2\'(\3\2\2\2(\16\3\2\2\2)+")
+        buf.write("\7\"\2\2*)\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\20\3")
+        buf.write("\2\2\2\7\2\37!\',\2")
         return buf.getvalue()
 
 
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