Merge PR #11314: Convert productionlists in the Gallina chapter up to the Vernacular section to prodns

Reviewed-by: Zimmi48

5 files changed, 56 insertions, 30 deletions

diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g
index 905b52525a..f9cf26a21e 100644
--- a/doc/tools/coqrst/notations/TacticNotations.g
+++ b/doc/tools/coqrst/notations/TacticNotations.g
@@ -42,7 +42,8 @@ LALT: '{|';
 LGROUP: '{+' | '{*' | '{?';
 LBRACE: '{';
 RBRACE: '}';
-ESCAPED: '%{' | '%}' | '%|';
+// todo: need a cleaner way to escape the 3-character strings here
+ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{';
 PIPE: '|';
 ATOM: '@' | '_' | ~[@_{}| ]+;
 ID: '@' ('_'? [a-zA-Z0-9])+;
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py
index e3a115e32a..7bda849010 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.py
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py
@@ -8,33 +8,35 @@ import sys
 def serializedATN():
     with StringIO() as buf:
         buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\f")
-        buf.write("M\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
+        buf.write("S\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
         buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\3\2\3\2\3\2\3\3\3\3")
         buf.write("\3\3\3\3\3\3\3\3\5\3!\n\3\3\4\3\4\3\5\3\5\3\6\3\6\3\6")
-        buf.write("\3\6\3\6\3\6\5\6-\n\6\3\7\3\7\3\b\3\b\6\b\63\n\b\r\b\16")
-        buf.write("\b\64\5\b\67\n\b\3\t\3\t\5\t;\n\t\3\t\6\t>\n\t\r\t\16")
-        buf.write("\t?\3\n\3\n\3\n\6\nE\n\n\r\n\16\nF\3\13\6\13J\n\13\r\13")
-        buf.write("\16\13K\2\2\f\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13")
-        buf.write("\25\f\3\2\5\4\2BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2V\2")
-        buf.write("\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3")
-        buf.write("\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2")
-        buf.write("\2\2\2\25\3\2\2\2\3\27\3\2\2\2\5 \3\2\2\2\7\"\3\2\2\2")
-        buf.write("\t$\3\2\2\2\13,\3\2\2\2\r.\3\2\2\2\17\66\3\2\2\2\218\3")
-        buf.write("\2\2\2\23A\3\2\2\2\25I\3\2\2\2\27\30\7}\2\2\30\31\7~\2")
-        buf.write("\2\31\4\3\2\2\2\32\33\7}\2\2\33!\7-\2\2\34\35\7}\2\2\35")
-        buf.write("!\7,\2\2\36\37\7}\2\2\37!\7A\2\2 \32\3\2\2\2 \34\3\2\2")
-        buf.write("\2 \36\3\2\2\2!\6\3\2\2\2\"#\7}\2\2#\b\3\2\2\2$%\7\177")
-        buf.write("\2\2%\n\3\2\2\2&\'\7\'\2\2\'-\7}\2\2()\7\'\2\2)-\7\177")
-        buf.write("\2\2*+\7\'\2\2+-\7~\2\2,&\3\2\2\2,(\3\2\2\2,*\3\2\2\2")
-        buf.write("-\f\3\2\2\2./\7~\2\2/\16\3\2\2\2\60\67\t\2\2\2\61\63\n")
-        buf.write("\3\2\2\62\61\3\2\2\2\63\64\3\2\2\2\64\62\3\2\2\2\64\65")
-        buf.write("\3\2\2\2\65\67\3\2\2\2\66\60\3\2\2\2\66\62\3\2\2\2\67")
-        buf.write("\20\3\2\2\28=\7B\2\29;\7a\2\2:9\3\2\2\2:;\3\2\2\2;<\3")
-        buf.write("\2\2\2<>\t\4\2\2=:\3\2\2\2>?\3\2\2\2?=\3\2\2\2?@\3\2\2")
-        buf.write("\2@\22\3\2\2\2AB\7a\2\2BD\7a\2\2CE\t\4\2\2DC\3\2\2\2E")
-        buf.write("F\3\2\2\2FD\3\2\2\2FG\3\2\2\2G\24\3\2\2\2HJ\7\"\2\2IH")
-        buf.write("\3\2\2\2JK\3\2\2\2KI\3\2\2\2KL\3\2\2\2L\26\3\2\2\2\13")
-        buf.write("\2 ,\64\66:?FK\2")
+        buf.write("\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\5\6\63\n\6\3\7\3")
+        buf.write("\7\3\b\3\b\6\b9\n\b\r\b\16\b:\5\b=\n\b\3\t\3\t\5\tA\n")
+        buf.write("\t\3\t\6\tD\n\t\r\t\16\tE\3\n\3\n\3\n\6\nK\n\n\r\n\16")
+        buf.write("\nL\3\13\6\13P\n\13\r\13\16\13Q\2\2\f\3\3\5\4\7\5\t\6")
+        buf.write("\13\7\r\b\17\t\21\n\23\13\25\f\3\2\5\4\2BBaa\6\2\"\"B")
+        buf.write("Baa}\177\5\2\62;C\\c|\2^\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\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3\2\2\2\3\27\3\2\2\2")
+        buf.write("\5 \3\2\2\2\7\"\3\2\2\2\t$\3\2\2\2\13\62\3\2\2\2\r\64")
+        buf.write("\3\2\2\2\17<\3\2\2\2\21>\3\2\2\2\23G\3\2\2\2\25O\3\2\2")
+        buf.write("\2\27\30\7}\2\2\30\31\7~\2\2\31\4\3\2\2\2\32\33\7}\2\2")
+        buf.write("\33!\7-\2\2\34\35\7}\2\2\35!\7,\2\2\36\37\7}\2\2\37!\7")
+        buf.write("A\2\2 \32\3\2\2\2 \34\3\2\2\2 \36\3\2\2\2!\6\3\2\2\2\"")
+        buf.write("#\7}\2\2#\b\3\2\2\2$%\7\177\2\2%\n\3\2\2\2&\'\7\'\2\2")
+        buf.write("\'\63\7}\2\2()\7\'\2\2)\63\7\177\2\2*+\7\'\2\2+\63\7~")
+        buf.write("\2\2,-\7b\2\2-.\7\'\2\2.\63\7}\2\2/\60\7B\2\2\60\61\7")
+        buf.write("\'\2\2\61\63\7}\2\2\62&\3\2\2\2\62(\3\2\2\2\62*\3\2\2")
+        buf.write("\2\62,\3\2\2\2\62/\3\2\2\2\63\f\3\2\2\2\64\65\7~\2\2\65")
+        buf.write("\16\3\2\2\2\66=\t\2\2\2\679\n\3\2\28\67\3\2\2\29:\3\2")
+        buf.write("\2\2:8\3\2\2\2:;\3\2\2\2;=\3\2\2\2<\66\3\2\2\2<8\3\2\2")
+        buf.write("\2=\20\3\2\2\2>C\7B\2\2?A\7a\2\2@?\3\2\2\2@A\3\2\2\2A")
+        buf.write("B\3\2\2\2BD\t\4\2\2C@\3\2\2\2DE\3\2\2\2EC\3\2\2\2EF\3")
+        buf.write("\2\2\2F\22\3\2\2\2GH\7a\2\2HJ\7a\2\2IK\t\4\2\2JI\3\2\2")
+        buf.write("\2KL\3\2\2\2LJ\3\2\2\2LM\3\2\2\2M\24\3\2\2\2NP\7\"\2\2")
+        buf.write("ON\3\2\2\2PQ\3\2\2\2QO\3\2\2\2QR\3\2\2\2R\26\3\2\2\2\13")
+        buf.write("\2 \62:<@ELQ\2")
         return buf.getvalue()
 
 
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py
index d9c5383774..1136ee4997 100644
--- a/doc/tools/coqrst/notations/html.py
+++ b/doc/tools/coqrst/notations/html.py
@@ -61,7 +61,7 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor):
             tags.sub(sub.getText()[1:])
 
     def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
-        tags.span(ctx.ESCAPED().getText()[1:])
+        tags.span(ctx.ESCAPED().getText().replace("%", ""))
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         text(" ")
diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py
index 93a7ec4683..23996b0d63 100644
--- a/doc/tools/coqrst/notations/plain.py
+++ b/doc/tools/coqrst/notations/plain.py
@@ -53,7 +53,7 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor):
         self.buffer.write("‘{}’".format(ctx.ID().getText()[1:]))
 
     def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
-        self.buffer.write(ctx.ESCAPED().getText()[1:])
+        self.buffer.write(ctx.ESCAPED().getText().replace("%", ""))
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         self.buffer.write(" ")
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py
index a42b583f2e..ab18d136b8 100644
--- a/doc/tools/coqrst/notations/sphinx.py
+++ b/doc/tools/coqrst/notations/sphinx.py
@@ -75,10 +75,33 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
         sp += nodes.Text("}")
         return [sp]
 
+    def escape(self, atom):
+        node = nodes.inline("","")
+        while atom != "":
+            if atom[0] == "'":
+                node += nodes.raw("\\textquotesingle{}", "\\textquotesingle{}", format="latex")
+                atom = atom[1:]
+            elif atom[0] == "`":
+                node += nodes.raw("\\`{}", "\\`{}", format="latex")
+                atom = atom[1:]
+            else:
+                index_ap = atom.find("'")
+                index_bt = atom.find("`")
+                if index_ap == -1:
+                    index = index_bt
+                elif index_bt == -1:
+                    index = index_ap
+                else:
+                    index = min(index_ap, index_bt)
+                lit = atom if index == -1 else atom[:index]
+                node += nodes.inline(lit, lit)
+                atom = atom[len(lit):]
+        return node
+
     def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
         atom = ctx.ATOM().getText()
         sub = ctx.SUB()
-        node = nodes.inline(atom, atom)
+        node = self.escape(atom)
 
         if sub:
             sub_index = sub.getText()[2:]
@@ -104,7 +127,7 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
 
     def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
         escaped = ctx.ESCAPED().getText()
-        return [nodes.inline(escaped, escaped[1:])]
+        return [self.escape(escaped.replace("%", ""))]
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         return [nodes.Text(" ")]