Merging branch/2023-02-22/manual-rtd-theme for github pull request <https://github.com/ravenbrook/mps/pull/166>.

GitHub-reference: https://github.com/Ravenbrook/mps/issues/166

mps/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

mps/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

mps/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 %}

mps/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'],
     }

mps/manual/source/index.rst

@@ -1,7 +1,8 @@
-Memory Pool System
-##################
+Contents
+********
 
 .. toctree::
+    :caption: Memory Pool System
     :maxdepth: 2
 
     guide/index
@@ -10,11 +11,8 @@ Memory Pool System
     design/index
     design/old
 
-
-Appendices
-##########
-
 .. toctree::
+    :caption: Appendices
     :maxdepth: 1
 
     bib
@@ -25,10 +23,9 @@ Appendices
     contributing
     release
 
-* :ref:`genindex`
-
-
 .. toctree::
+    :caption: Memory Management Reference
+    :maxdepth: 2
     :hidden:
 
     mmref/index
@@ -36,3 +33,6 @@ Appendices
     mmref/faq
     mmref-copyright
     mmref/credit
+
+* :ref:`genindex`
+