Support in-line glossary entries and references

with an index

5 files changed, 75 insertions, 6 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
+--------------
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 57243207f0..9d51d2198a 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -472,8 +472,7 @@ class ProductionObject(CoqObject):
             op = "|"
             rhs = parts[1].strip()
         else:
-            nsplits = 2
-            parts = signature.split(maxsplit=nsplits)
+            parts = signature.split(maxsplit=2)
             if len(parts) != 3:
                 loc = os.path.basename(get_node_location(signode))
                 raise ExtensionError(ProductionObject.SIG_ERROR.format(loc, signature))
@@ -1116,6 +1115,19 @@ class IndexXRefRole(XRefRole):
                 title = index.localname
         return title, target
 
+class StdGlossaryIndex(Index):
+    name, localname, shortname = "glossindex", "Glossary", "terms"
+
+    def generate(self, docnames=None):
+        content = defaultdict(list)
+
+        for ((type, itemname), (docname, anchor)) in self.domain.data['objects'].items():
+            if type == 'term':
+                entries = content[itemname[0].lower()]
+                entries.append([itemname, 0, docname, anchor, '', '', ''])
+        content = sorted(content.items())
+        return content, False
+
 def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
     """A grammar production not included in a ``productionlist`` directive.
 
@@ -1132,7 +1144,7 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte
     """
     #pylint: disable=dangerous-default-value, unused-argument
     env = inliner.document.settings.env
-    targetid = 'grammar-token-{}'.format(text)
+    targetid = nodes.make_id('grammar-token-{}'.format(text))
     target = nodes.target('', '', ids=[targetid])
     inliner.document.note_explicit_target(target)
     code = nodes.literal(rawtext, text, role=typ.lower())
@@ -1143,6 +1155,35 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte
 
 GrammarProductionRole.role_name = "production"
 
+
+def GlossaryDefRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
+    """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.
+    """
+    #pylint: disable=dangerous-default-value, unused-argument
+    env = inliner.document.settings.env
+    std = env.domaindata['std']['objects']
+    key = ('term', text)
+
+    if key in std:
+        MSG = 'Duplicate object: {}; other is at {}'
+        msg = MSG.format(text, env.doc2path(std[key][0]))
+        inliner.document.reporter.warning(msg, line=lineno)
+
+    targetid = nodes.make_id('term-{}'.format(text))
+    std[key] = (env.docname, targetid)
+    target = nodes.target('', '', ids=[targetid], names=[text])
+    inliner.document.note_explicit_target(target)
+    node = nodes.inline(rawtext, '', target, nodes.Text(text), classes=['term-defn'])
+    set_role_source_info(inliner, lineno, node)
+    return [node], []
+
+GlossaryDefRole.role_name = "gdef"
+
 class CoqDomain(Domain):
     """A domain to document Coq code.
 
@@ -1305,18 +1346,23 @@ COQ_ADDITIONAL_DIRECTIVES = [CoqtopDirective,
                              InferenceDirective,
                              PreambleDirective]
 
-COQ_ADDITIONAL_ROLES = [GrammarProductionRole]
+COQ_ADDITIONAL_ROLES = [GrammarProductionRole,
+                        GlossaryDefRole]
 
 def setup(app):
     """Register the Coq domain"""
 
     # A few sanity checks:
     subdomains = set(obj.subdomain for obj in CoqDomain.directives.values())
-    assert subdomains.issuperset(chain(*(idx.subdomains for idx in CoqDomain.indices)))
-    assert subdomains.issubset(CoqDomain.roles.keys())
+    found = set (obj for obj in chain(*(idx.subdomains for idx in CoqDomain.indices)))
+    assert subdomains.issuperset(found), "Missing subdomains: {}".format(found.difference(subdomains))
+
+    assert subdomains.issubset(CoqDomain.roles.keys()), \
+        "Missing from CoqDomain.roles: {}".format(subdomains.difference(CoqDomain.roles.keys()))
 
     # Add domain, directives, and roles
     app.add_domain(CoqDomain)
+    app.add_index_to_domain('std', StdGlossaryIndex)
 
     for role in COQ_ADDITIONAL_ROLES:
         app.add_role(role.role_name, role)