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

Ack-by: Zimmi48
Ack-by: cpitclaudel

3 files changed, 75 insertions, 15 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 */