docs: ref redirector (#15432)

Makes the HTML builder generate a _refs.html file that redirects (global) refs (when provided as a hash i.e. `_refs.html#some-ref`) to the appropriate document. This allows tools (e.g. #15431) to link to well-known refs.
python · Jun 24, 2023 · 32abe02 · 32abe02
1 parent e5a5b33
commit 32abe02
Show file tree

Hide file tree

Showing 2 changed files with 51 additions and 1 deletion.
diff --git a/docs/source/conf.py b/docs/source/conf.py
@@ -35,7 +35,7 @@
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
-extensions = ["sphinx.ext.intersphinx"]
+extensions = ["sphinx.ext.intersphinx", "docs.source.html_builder"]
 
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ["_templates"]

diff --git a/docs/source/html_builder.py b/docs/source/html_builder.py
@@ -0,0 +1,50 @@
+from __future__ import annotations
+
+import json
+import textwrap
+from pathlib import Path
+from typing import Any
+
+from sphinx.addnodes import document
+from sphinx.application import Sphinx
+from sphinx.builders.html import StandaloneHTMLBuilder
+
+
+class MypyHTMLBuilder(StandaloneHTMLBuilder):
+    def __init__(self, app: Sphinx) -> None:
+        super().__init__(app)
+        self._ref_to_doc = {}
+
+    def write_doc(self, docname: str, doctree: document) -> None:
+        super().write_doc(docname, doctree)
+        self._ref_to_doc.update({_id: docname for _id in doctree.ids})
+
+    def _write_ref_redirector(self) -> None:
+        p = Path(self.outdir) / "_refs.html"
+        data = f"""
+        <html>
+        <body>
+        <script>
+        const ref_to_doc = {json.dumps(self._ref_to_doc)};
+        const hash = window.location.hash.substring(1);
+        const doc = ref_to_doc[hash];
+        if (doc) {{
+            window.location.href = doc + '.html' + '#' + hash;
+        }} else {{
+            window.document.innerText = 'Unknown reference: ' + hash;
+        }}
+        </script>
+        </body>
+        </html>
+        """
+        p.write_text(textwrap.dedent(data))
+
+    def finish(self) -> None:
+        super().finish()
+        self._write_ref_redirector()
+
+
+def setup(app: Sphinx) -> dict[str, Any]:
+    app.add_builder(MypyHTMLBuilder, override=True)
+
+    return {"version": "0.1", "parallel_read_safe": True, "parallel_write_safe": True}