Merge PR #12150: Support in-line glossary definitions and references with an index

Ack-by: Zimmi48

4 files changed, 23 insertions, 0 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 0802b5d0b4..e20469bb8b 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -358,6 +358,13 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
     and reference its tokens using ``:token:`…```.
 
+``:gdef:`` Marks the definition of a glossary term inline in the text.  Matching :term:`XXX`
+    constructs will link to it.  The term will also appear in the Glossary Index.
+
+    Example::
+
+       A :gdef:`prime` number is divisible only by itself and 1.
+
 Common mistakes
 ===============
 
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 733a73bd21..9546f7107e 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -215,6 +215,14 @@
     margin-bottom: 0.28em;
 }
 
+.term-defn {
+    font-style: italic;
+}
+
+.std-term {
+    color: #2980B9;  /* override if :visited */
+}
+
 /* We can't display nested blocks otherwise */
 code, .rst-content tt, .rst-content code {
     background: transparent !important;
diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst
index 2ece726df7..c8b2cf46dc 100644
--- a/doc/sphinx/appendix/indexes/index.rst
+++ b/doc/sphinx/appendix/indexes/index.rst
@@ -17,6 +17,7 @@ find what you are looking for.
    ../../coq-optindex
    ../../coq-exnindex
    ../../coq-attrindex
+   ../../std-glossindex
 
 For reference, here are direct links to the documentation of:
 
diff --git a/doc/sphinx/std-glossindex.rst b/doc/sphinx/std-glossindex.rst
new file mode 100644
index 0000000000..3f085ca737
--- /dev/null
+++ b/doc/sphinx/std-glossindex.rst
@@ -0,0 +1,7 @@
+:orphan:
+
+.. hack to get index in TOC
+
+--------------
+Glossary index
+--------------