Merging branch/2023-02-22/manual-rtd-theme for GitHub pull request #166 <#166>.

Author: rptb1

manual/Makefile

@@ -159,10 +159,10 @@ doctest: $(SPHINXBUILD)
 	      "results in $(BUILDDIR)/doctest/output.txt."
 
 .PHONY: tools
-tools: tool/bin/pip requirements.pip
-	tool/bin/pip install -r requirements.pip
+tools: $(SPHINXBUILD)
 
-tool/bin/sphinx-build: tools
+$(SPHINXBUILD): tool/bin/pip requirements.pip
+	tool/bin/pip install -r requirements.pip
 
 tool/bin/pip:
 	$(PYTHON) -mvenv tool

manual/requirements.pip

@@ -1,4 +1,4 @@
-# manual/requirements.txt -- MPS manual build requirements for pip
+# manual/requirements.pip -- MPS manual build requirements for pip
 
-# Layout breaks in Sphinx >= 5.  See <https://github.com/Ravenbrook/mps/issues/121>.
-sphinx >= 4, < 5
+sphinx
+sphinx-rtd-theme

manual/source/_templates/layout.html

@@ -0,0 +1,40 @@
+{# manual/source/_templates/layout.html -- add index to manual sidebar.
+ #
+ # See https://stackoverflow.com/a/37843854 .
+ #}
+
+{% extends "!layout.html" %}
+
+  {% block menu %}
+    {{ super() }}
+
+<p class="caption" role="heading">
+  <span class="caption-text">Indices and tables</span>
+</p>
+
+<ul>
+
+  {# The class toctree-l1 seems to correspond to list items generated
+     by a Sphinx toctree directive that are at depth 1.  I have not
+     found documented confirmation of this but it is confirmed
+     `_toctree_add_classes
+     <https://github.com/sphinx-doc/sphinx/blob/bb74aec2b6aa1179868d83134013450c9ff9d4d6/sphinx/environment/adapters/toctree.py#L403-L430>`_
+     in the Sphinx source code.  If the list layout goes wonky, this
+     might be to blame.  RB 2023-10-20. #}
+
+  <li class="toctree-l1">
+
+    <a class="reference internal" href="{{pathto('genindex.html', 1)}}">Index</a>
+
+    {# Module index and search page aren't used in the MPS manual but
+       might be in future.  This is how they might be added. #}
+
+    {# <a class="reference internal" href="{{pathto('modindex.html', 1)}}">Module Index</a> #}
+
+    {# <a class="reference internal" href="{{pathto('search.html', 1)}}">Search Page</a> #}
+
+  </li>
+
+</ul>
+
+  {% endblock %}

manual/source/conf.py

@@ -37,7 +37,17 @@
 else:
     project = u'Memory Pool System'
     master_doc = 'index'
-    html_theme = 'mps'
+    # We use the Read the Docs theme for Sphinx for smooth publishing
+    # at readthedocs.io, low maintenance overheads, local search, etc.
+    # See primarily `GitHub issue #98
+    # <https://github.com/Ravenbrook/mps/issues/98>`_ but also `GitHub
+    # issue #121 <https://github.com/Ravenbrook/mps/issues/121>`_ .
+    # See <https://sphinx-rtd-theme.readthedocs.io/> for theme
+    # documentation.
+    html_theme = 'sphinx_rtd_theme'
+    html_theme_options = {
+        'includehidden': False,
+    }
     html_sidebars = {
         '**': ['localtoc.html', 'relations.html', 'links.html', 'contact.html'],
     }