[doc] Add a README to doc/sphinx/

The readme is auto-generated by combining introductory text with the docstrings
in coqdomain.py.

2 files changed, 63 insertions, 2 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 75ed70e08..3cad394e6 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -433,12 +433,15 @@ class CoqtopDirective(Directive):
 
     Here is a list of permissible options:
 
-    Display
+    - Display options
+
       - ``all``: Display input and output
       - ``in``: Display only input
       - ``out``: Display only output
       - ``none``: Display neither (useful for setup commands)
-    Behaviour
+
+    - Behavior options
+
       - ``reset``: Send a ``Reset Initial`` command before running this block
       - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after
         running all the commands in this block
diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py
new file mode 100755
index 000000000..050ca4956
--- /dev/null
+++ b/doc/tools/coqrst/regen_readme.py
@@ -0,0 +1,58 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+
+"""Rebuild README.rst from README.template.rst."""
+
+import re
+from os import sys, path
+
+SCRIPT_DIR = path.dirname(path.abspath(__file__))
+if __name__ == "__main__" and __package__ is None:
+    sys.path.append(path.dirname(SCRIPT_DIR))
+
+import sphinx
+from coqrst import coqdomain
+
+README_ROLES_MARKER = "[ROLES]"
+README_OBJECTS_MARKER = "[OBJECTS]"
+README_DIRECTIVES_MARKER = "[DIRECTIVES]"
+
+FIRST_LINE_BLANKS = re.compile("^(.*)\n *\n")
+def format_docstring(template, obj, *strs):
+    docstring = obj.__doc__.strip()
+    strs = strs + (FIRST_LINE_BLANKS.sub(r"\1\n", docstring),)
+    return template.format(*strs)
+
+SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/")
+README_PATH = path.join(SPHINX_DIR, "README.rst")
+README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst")
+
+def notation_symbol(d):
+    return " :black_nib:" if issubclass(d, coqdomain.NotationObject) else ""
+
+def regen_readme():
+    objects_docs = [format_docstring("``.. {}::``{} {}", obj, objname, notation_symbol(obj))
+                    for objname, obj in sorted(coqdomain.CoqDomain.directives.items())]
+
+    roles = ([(name, cls)
+              for name, cls in sorted(coqdomain.CoqDomain.roles.items())
+              if not isinstance(cls, (sphinx.roles.XRefRole, coqdomain.IndexXRefRole))] +
+             [(fn.role_name, fn)
+              for fn in coqdomain.COQ_ADDITIONAL_ROLES])
+    roles_docs = [format_docstring("``:{}:`` {}", role, name)
+                  for (name, role) in roles]
+
+    directives_docs = [format_docstring("``.. {}::`` {}", d, d.directive_name)
+                       for d in coqdomain.COQ_ADDITIONAL_DIRECTIVES]
+
+    with open(README_TEMPLATE_PATH, encoding="utf-8") as readme:
+        contents = readme.read()
+
+    with open(README_PATH, mode="w", encoding="utf-8") as readme:
+        readme.write(contents
+                     .replace(README_ROLES_MARKER, "\n\n".join(roles_docs))
+                     .replace(README_OBJECTS_MARKER, "\n\n".join(objects_docs))
+                     .replace(README_DIRECTIVES_MARKER, "\n\n".join(directives_docs)))
+
+if __name__ == '__main__':
+    regen_readme()