From 99e239172dbd384418500554a6d8b4a058c3545b Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 21 Apr 2020 13:13:43 -0700
Subject: Support in-line glossary entries and references with an index

---
 doc/sphinx/README.rst                 | 7 +++++++
 doc/sphinx/_static/notations.css      | 8 ++++++++
 doc/sphinx/appendix/indexes/index.rst | 1 +
 doc/sphinx/std-glossindex.rst         | 7 +++++++
 4 files changed, 23 insertions(+)
 create mode 100644 doc/sphinx/std-glossindex.rst

(limited to 'doc/sphinx')

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
+--------------
-- 
cgit v1.2.3