Merge PR #11183: Enhance prodn in .rst doc files to support multiple productions in a prodn

Ack-by: Zimmi48
Ack-by: cpitclaudel

5 files changed, 158 insertions, 47 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 549598b187..f504678ef9 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -143,22 +143,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
           application of a tactic.
 
 ``.. prodn::`` A grammar production.
-    This is useful if you intend to document individual grammar productions.
-    Otherwise, use Sphinx's `production lists
+    Use prodn to document individual grammar productions instead of Sphinx
+    `production lists
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
 
-    Unlike ``.. productionlist``\ s, this directive accepts notation syntax.
-
-
-    Usage::
-
-       .. prodn:: token += production
-       .. prodn:: token ::= production
+    prodn displays multiple productions together with alignment similar to ``.. productionlist``,
+    i.e. displayed in 3 columns, however
+    unlike ``.. productionlist``\ s, this directive accepts notation syntax.
 
     Example::
 
-        .. prodn:: term += let: @pattern := @term in @term
         .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
+        term += let: @pattern := @term in @term
+        | second_production
+
+       The first line defines "occ_switch", which must be unique in the document.  The second
+       references but doesn't define "term".  The third form is for continuing the
+       definition of a nonterminal when it has multiple productions.  It leaves the first
+       column in the output blank.
 
 ``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values.
     Example::
diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty
index 3548b8754c..8612e51aa5 100644
--- a/doc/sphinx/_static/coqnotations.sty
+++ b/doc/sphinx/_static/coqnotations.sty
@@ -70,8 +70,23 @@
 \newcssclass{notation}{\nnotation{#1}}
 \newcssclass{repeat}{\nrepeat{#1}}
 \newcssclass{repeat-wrapper}{\nwrapper{#1}}
+\newcssclass{repeat-wrapper-with-sub}{\nwrapper{#1}}
 \newcssclass{hole}{\nhole{#1}}
 \newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}}
 \newcssclass{alternative-block}{#1}
 \newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}}
 \newcssclass{alternative-separator}{\quad\naltsep{}\quad}
+\newcssclass{prodn-table}{%
+  \begin{savenotes}
+  \sphinxattablestart
+  \begin{tabulary}{\linewidth}[t]{lLL}
+  #1
+  \end{tabulary}
+  \par
+  \sphinxattableend
+  \end{savenotes}}
+% latex puts targets 1 line below where they should be; prodn-target corrects for this
+\newcssclass{prodn-target}{\raisebox{\dimexpr \nscriptsize \relax}{#1}}
+\newcssclass{prodn-cell-nonterminal}{#1 &}
+\newcssclass{prodn-cell-op}{#1 &}
+\newcssclass{prodn-cell-production}{#1\\}
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 4a5fa0b328..d654479b07 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -85,7 +85,8 @@
     padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
 }
 
-.notation .repeat-wrapper {
+.notation .repeat-wrapper,
+.notation .repeat-wrapper-with-sub {
     display: inline-block;
     position: relative;
     margin-right: 0.4em; /* Space for the right half of the sub- and sup-scripts */
@@ -165,10 +166,52 @@
 /* Overrides */
 /*************/
 
-.rst-content table.docutils td, .rst-content table.docutils th {
-    padding: 8px; /* Reduce horizontal padding */
-    border-left: none;
-    border-right: none;
+.prodn-table {
+    display: table;
+    margin: 1.5em 0px;
+    vertical-align: baseline;
+    font-weight: bold;
+}
+
+.prodn-column-group  {
+    display: table-column-group;
+}
+
+.prodn-column {
+    display: table-column;
+}
+
+.prodn-row-group {
+    display: table-row-group;
+}
+
+.prodn-row {
+    display: table-row;
+}
+
+.prodn-cell-nonterminal,
+.prodn-cell-op,
+.prodn-cell-production
+{
+    display: table-cell;
+}
+
+.prodn-cell-nonterminal {
+    padding-right: 0.49em;
+}
+
+.prodn-cell-op {
+    padding-right: 0.90em;
+    font-weight: normal;
+}
+
+.prodn-table .notation > .repeat-wrapper {
+    margin-top: 0.28em;
+}
+
+.prodn-table .notation > .repeat-wrapper-with-sub {
+    margin-top: 0.28em;
+    margin-bottom: 0.28em;
 }
 
 /* We can't display nested blocks otherwise */
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index eff70bdac5..b9faeacad7 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -403,55 +403,60 @@ class TableObject(NotationObject):
 class ProductionObject(CoqObject):
     r"""A grammar production.
 
-    This is useful if you intend to document individual grammar productions.
-    Otherwise, use Sphinx's `production lists
+    Use prodn to document individual grammar productions instead of Sphinx
+    `production lists
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
 
-    Unlike ``.. productionlist``\ s, this directive accepts notation syntax.
-
-
-    Usage::
-
-       .. prodn:: token += production
-       .. prodn:: token ::= production
+    prodn displays multiple productions together with alignment similar to ``.. productionlist``,
+    i.e. displayed in 3 columns, however
+    unlike ``.. productionlist``\ s, this directive accepts notation syntax.
 
     Example::
 
-        .. prodn:: term += let: @pattern := @term in @term
         .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
+        term += let: @pattern := @term in @term
+        | second_production
+
+       The first line defines "occ_switch", which must be unique in the document.  The second
+       references but doesn't define "term".  The third form is for continuing the
+       definition of a nonterminal when it has multiple productions.  It leaves the first
+       column in the output blank.
 
     """
     subdomain = "prodn"
     #annotation = "Grammar production"
 
+    # handle_signature is called for each line of input in the prodn::
+    # 'signatures' accumulates them in order to combine the lines into a single table:
+    signatures = None
+
     def _render_signature(self, signature, signode):
         raise NotImplementedError(self)
 
     SIG_ERROR = ("{}: Invalid syntax in ``.. prodn::`` directive"
                  + "\nExpected ``name ::= ...`` or ``name += ...``"
-                 + " (e.g. ``pattern += constr:(@ident)``)")
+                 + " (e.g. ``pattern += constr:(@ident)``)\n"
+                 + "  in `{}`")
 
     def handle_signature(self, signature, signode):
-        nsplits = 2
-        parts = signature.split(maxsplit=nsplits)
-        if len(parts) != 3:
-            loc = os.path.basename(get_node_location(signode))
-            raise ExtensionError(ProductionObject.SIG_ERROR.format(loc))
-
-        lhs, op, rhs = (part.strip() for part in parts)
-        if op not in ["::=", "+="]:
-            loc = os.path.basename(get_node_location(signode))
-            raise ExtensionError(ProductionObject.SIG_ERROR.format(loc))
-
-        self._render_annotation(signode)
-
-        lhs_op = '{} {} '.format(lhs, op)
-        lhs_node = nodes.literal(lhs_op, lhs_op)
-
-        position = self.state_machine.get_source_and_line(self.lineno)
-        rhs_node = notation_to_sphinx(rhs, *position)
-        signode += addnodes.desc_name(signature, '', lhs_node, rhs_node)
+        parts = signature.split(maxsplit=1)
+        if parts[0].strip() == "|" and len(parts) == 2:
+            lhs = ""
+            op = "|"
+            rhs = parts[1].strip()
+        else:
+            nsplits = 2
+            parts = signature.split(maxsplit=nsplits)
+            if len(parts) != 3:
+                loc = os.path.basename(get_node_location(signode))
+                raise ExtensionError(ProductionObject.SIG_ERROR.format(loc, signature))
+            else:
+                lhs, op, rhs = (part.strip() for part in parts)
+                if op not in ["::=", "+="]:
+                    loc = os.path.basename(get_node_location(signode))
+                    raise ExtensionError(ProductionObject.SIG_ERROR.format(loc, signature))
 
+        self.signatures.append((lhs, op, rhs))
         return ('token', lhs) if op == '::=' else None
 
     def _add_index_entry(self, name, target):
@@ -468,6 +473,49 @@ class ProductionObject(CoqObject):
         self._warn_if_duplicate_name(objects, name)
         objects[name] = env.docname, targetid
 
+    def run(self):
+        self.signatures = []
+        indexnode = super().run()[0]  # makes calls to handle_signature
+
+        table = nodes.inline(classes=['prodn-table'])
+        tgroup = nodes.inline(classes=['prodn-column-group'])
+        for i in range(3):
+            tgroup += nodes.inline(classes=['prodn-column'])
+        table += tgroup
+        tbody = nodes.inline(classes=['prodn-row-group'])
+        table += tbody
+
+        # create rows
+        for signature in self.signatures:
+            lhs, op, rhs = signature
+            position = self.state_machine.get_source_and_line(self.lineno)
+
+            row = nodes.inline(classes=['prodn-row'])
+            entry = nodes.inline(classes=['prodn-cell-nonterminal'])
+            if lhs != "":
+                target_name = 'grammar-token-' + lhs
+                target = nodes.target('', '', ids=[target_name], names=[target_name])
+                # putting prodn-target on the target node won't appear in the tex file
+                inline = nodes.inline(classes=['prodn-target'])
+                inline += target
+                entry += inline
+                entry += notation_to_sphinx('@'+lhs, *position)
+            else:
+                entry += nodes.literal('', '')
+            row += entry
+
+            entry = nodes.inline(classes=['prodn-cell-op'])
+            entry += nodes.literal(op, op)
+            row += entry
+
+            entry = nodes.inline(classes=['prodn-cell-production'])
+            entry += notation_to_sphinx(rhs, *position)
+            row += entry
+
+            tbody += row
+
+        return [indexnode, table] # only this node goes into the doc
+
 class ExceptionObject(NotationObject):
     """An error raised by a Coq command or tactic.
 
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py
index 4ca0a2ef83..a42b583f2e 100644
--- a/doc/tools/coqrst/notations/sphinx.py
+++ b/doc/tools/coqrst/notations/sphinx.py
@@ -45,7 +45,11 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
     def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
         # Uses inline nodes instead of subscript and superscript to ensure that
         # we get the right customization hooks at the LaTeX level
-        wrapper = nodes.inline('', '', classes=['repeat-wrapper'])
+        separator = ctx.ATOM() or ctx.PIPE()
+        # I wanted to have 2 independent classes "repeat-wrapper" and "with-sub" here,
+        # but that breaks the latex build (invalid .tex file)
+        classes = 'repeat-wrapper-with-sub' if separator  else 'repeat-wrapper'
+        wrapper = nodes.inline('', '', classes=[classes])
 
         children = self.visitChildren(ctx)
         if len(children) == 1 and self.is_alternative(children[0]):
@@ -58,7 +62,6 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
         repeat_marker = ctx.LGROUP().getText()[1]
         wrapper += nodes.inline(repeat_marker, repeat_marker, classes=['notation-sup'])
 
-        separator = ctx.ATOM() or ctx.PIPE()
         if separator:
             sep = separator.getText()
             wrapper += nodes.inline(sep, sep, classes=['notation-sub'])