about summary refs log tree commit diff
diff options
context:
space:
mode:
authorTshepang Mbambo <hopsi@tuta.io>2025-07-17 06:09:15 +0200
committerTshepang Mbambo <hopsi@tuta.io>2025-07-28 09:26:08 +0200
commit3e6f950d66008a7a15f38d10d5b19707c06602c7 (patch)
tree8c7235a6b76fba525a82e4a42785628b186c1ff5
parentbfca77bf84e25470210624ecad0cecfc4e791854 (diff)
downloadrust-3e6f950d66008a7a15f38d10d5b19707c06602c7.tar.gz
rust-3e6f950d66008a7a15f38d10d5b19707c06602c7.zip
avoid the need to specify if toc should be generated
- this removes one external dependency, mdbook-toc
- this steals code from rustc book
-rw-r--r--src/doc/rustc-dev-guide/.github/workflows/ci.yml4
-rw-r--r--src/doc/rustc-dev-guide/README.md6
-rw-r--r--src/doc/rustc-dev-guide/book.toml11
-rw-r--r--src/doc/rustc-dev-guide/pagetoc.css84
-rw-r--r--src/doc/rustc-dev-guide/pagetoc.js104
5 files changed, 198 insertions, 11 deletions
diff --git a/src/doc/rustc-dev-guide/.github/workflows/ci.yml b/src/doc/rustc-dev-guide/.github/workflows/ci.yml
index daf5223cbd4..6eabb999fb0 100644
--- a/src/doc/rustc-dev-guide/.github/workflows/ci.yml
+++ b/src/doc/rustc-dev-guide/.github/workflows/ci.yml
@@ -17,7 +17,6 @@ jobs:
       MDBOOK_VERSION: 0.4.48
       MDBOOK_LINKCHECK2_VERSION: 0.9.1
       MDBOOK_MERMAID_VERSION: 0.12.6
-      MDBOOK_TOC_VERSION: 0.11.2
       MDBOOK_OUTPUT__LINKCHECK__FOLLOW_WEB_LINKS: ${{ github.event_name != 'pull_request' }}
       DEPLOY_DIR: book/html
       BASE_SHA: ${{ github.event.pull_request.base.sha }}
@@ -34,7 +33,7 @@ jobs:
         with:
           path: |
             ~/.cargo/bin
-          key: ${{ runner.os }}-${{ env.MDBOOK_VERSION }}--${{ env.MDBOOK_LINKCHECK2_VERSION }}--${{ env.MDBOOK_TOC_VERSION }}--${{ env.MDBOOK_MERMAID_VERSION }}
+          key: ${{ runner.os }}-${{ env.MDBOOK_VERSION }}--${{ env.MDBOOK_LINKCHECK2_VERSION }}--${{ env.MDBOOK_MERMAID_VERSION }}
 
       - name: Restore cached Linkcheck
         if: github.event_name == 'schedule'
@@ -57,7 +56,6 @@ jobs:
         run: |
           cargo install mdbook --version ${{ env.MDBOOK_VERSION }}
           cargo install mdbook-linkcheck2 --version ${{ env.MDBOOK_LINKCHECK2_VERSION }}
-          cargo install mdbook-toc --version ${{ env.MDBOOK_TOC_VERSION }}
           cargo install mdbook-mermaid --version ${{ env.MDBOOK_MERMAID_VERSION }}
 
       - name: Check build
diff --git a/src/doc/rustc-dev-guide/README.md b/src/doc/rustc-dev-guide/README.md
index 5932da467ab..1ad895aeda2 100644
--- a/src/doc/rustc-dev-guide/README.md
+++ b/src/doc/rustc-dev-guide/README.md
@@ -43,7 +43,7 @@ rustdocs][rustdocs].
 To build a local static HTML site, install [`mdbook`](https://github.com/rust-lang/mdBook) with:
 
 ```
-cargo install mdbook mdbook-linkcheck2 mdbook-toc mdbook-mermaid
+cargo install mdbook mdbook-linkcheck2 mdbook-mermaid
 ```
 
 and execute the following command in the root of the repository:
@@ -67,8 +67,8 @@ ENABLE_LINKCHECK=1 mdbook serve
 
 ### Table of Contents
 
-We use `mdbook-toc` to auto-generate TOCs for long sections. You can invoke the preprocessor by
-including the `<!-- toc -->` marker at the place where you want the TOC.
+Each page has a TOC that is automatically generated by `pagetoc.js`.
+There is an associated `pagetoc.css`, for styling.
 
 ## Synchronizing josh subtree with rustc
 
diff --git a/src/doc/rustc-dev-guide/book.toml b/src/doc/rustc-dev-guide/book.toml
index b84b1e7548a..daf237ed908 100644
--- a/src/doc/rustc-dev-guide/book.toml
+++ b/src/doc/rustc-dev-guide/book.toml
@@ -6,17 +6,18 @@ description = "A guide to developing the Rust compiler (rustc)"
 [build]
 create-missing = false
 
-[preprocessor.toc]
-command = "mdbook-toc"
-renderer = ["html"]
-
 [preprocessor.mermaid]
 command = "mdbook-mermaid"
 
 [output.html]
 git-repository-url = "https://github.com/rust-lang/rustc-dev-guide"
 edit-url-template = "https://github.com/rust-lang/rustc-dev-guide/edit/master/{path}"
-additional-js = ["mermaid.min.js", "mermaid-init.js"]
+additional-js = [
+  "mermaid.min.js",
+  "mermaid-init.js",
+  "pagetoc.js",
+]
+additional-css = ["pagetoc.css"]
 
 [output.html.search]
 use-boolean-and = true
diff --git a/src/doc/rustc-dev-guide/pagetoc.css b/src/doc/rustc-dev-guide/pagetoc.css
new file mode 100644
index 00000000000..fa709194f37
--- /dev/null
+++ b/src/doc/rustc-dev-guide/pagetoc.css
@@ -0,0 +1,84 @@
+/* Inspired by https://github.com/JorelAli/mdBook-pagetoc/tree/98ee241 (under WTFPL) */
+
+:root {
+    --toc-width: 270px;
+    --center-content-toc-shift: calc(-1 * var(--toc-width) / 2);
+}
+
+.nav-chapters {
+    /* adjust width of buttons that bring to the previous or the next page */
+    min-width: 50px;
+}
+
+@media only screen {
+    @media (max-width: 1179px) {
+        .sidebar-hidden #sidetoc {
+            display: none;
+        }
+    }
+
+    @media (max-width: 1439px) {
+        .sidebar-visible #sidetoc {
+            display: none;
+        }
+    }
+
+    @media (1180px <= width <= 1439px) {
+        .sidebar-hidden main {
+            position: relative;
+            left: var(--center-content-toc-shift);
+        }
+    }
+
+    @media (1440px <= width <= 1700px) {
+        .sidebar-visible main {
+            position: relative;
+            left: var(--center-content-toc-shift);
+        }
+    }
+
+    #sidetoc {
+        margin-left: calc(100% + 20px);
+    }
+    #pagetoc {
+        position: fixed;
+        /* adjust TOC width */
+        width: var(--toc-width);
+        height: calc(100vh - var(--menu-bar-height) - 0.67em * 4);
+        overflow: auto;
+    }
+    #pagetoc a {
+        border-left: 1px solid var(--sidebar-bg);
+        color: var(--fg);
+        display: block;
+        padding-bottom: 5px;
+        padding-top: 5px;
+        padding-left: 10px;
+        text-align: left;
+        text-decoration: none;
+    }
+    #pagetoc a:hover,
+    #pagetoc a.active {
+        background: var(--sidebar-bg);
+        color: var(--sidebar-active) !important;
+    }
+    #pagetoc .active {
+        background: var(--sidebar-bg);
+        color: var(--sidebar-active);
+    }
+    #pagetoc .pagetoc-H2 {
+        padding-left: 20px;
+    }
+    #pagetoc .pagetoc-H3 {
+        padding-left: 40px;
+    }
+    #pagetoc .pagetoc-H4 {
+        padding-left: 60px;
+    }
+}
+
+@media print {
+    #sidetoc {
+        display: none;
+    }
+}
diff --git a/src/doc/rustc-dev-guide/pagetoc.js b/src/doc/rustc-dev-guide/pagetoc.js
new file mode 100644
index 00000000000..927a5b10749
--- /dev/null
+++ b/src/doc/rustc-dev-guide/pagetoc.js
@@ -0,0 +1,104 @@
+// Inspired by https://github.com/JorelAli/mdBook-pagetoc/tree/98ee241 (under WTFPL)
+
+let activeHref = location.href;
+function updatePageToc(elem = undefined) {
+    let selectedPageTocElem = elem;
+    const pagetoc = document.getElementById("pagetoc");
+
+    function getRect(element) {
+        return element.getBoundingClientRect();
+    }
+
+    function overflowTop(container, element) {
+        return getRect(container).top - getRect(element).top;
+    }
+
+    function overflowBottom(container, element) {
+        return getRect(container).bottom - getRect(element).bottom;
+    }
+
+    // We've not selected a heading to highlight, and the URL needs updating
+    // so we need to find a heading based on the URL
+    if (selectedPageTocElem === undefined && location.href !== activeHref) {
+        activeHref = location.href;
+        for (const pageTocElement of pagetoc.children) {
+            if (pageTocElement.href === activeHref) {
+                selectedPageTocElem = pageTocElement;
+            }
+        }
+    }
+
+    // We still don't have a selected heading, let's try and find the most
+    // suitable heading based on the scroll position
+    if (selectedPageTocElem === undefined) {
+        const margin = window.innerHeight / 3;
+
+        const headers = document.getElementsByClassName("header");
+        for (let i = 0; i < headers.length; i++) {
+            const header = headers[i];
+            if (selectedPageTocElem === undefined && getRect(header).top >= 0) {
+                if (getRect(header).top < margin) {
+                    selectedPageTocElem = header;
+                } else {
+                    selectedPageTocElem = headers[Math.max(0, i - 1)];
+                }
+            }
+            // a very long last section's heading is over the screen
+            if (selectedPageTocElem === undefined && i === headers.length - 1) {
+                selectedPageTocElem = header;
+            }
+        }
+    }
+
+    // Remove the active flag from all pagetoc elements
+    for (const pageTocElement of pagetoc.children) {
+        pageTocElement.classList.remove("active");
+    }
+
+    // If we have a selected heading, set it to active and scroll to it
+    if (selectedPageTocElem !== undefined) {
+        for (const pageTocElement of pagetoc.children) {
+            if (selectedPageTocElem.href.localeCompare(pageTocElement.href) === 0) {
+                pageTocElement.classList.add("active");
+                if (overflowTop(pagetoc, pageTocElement) > 0) {
+                    pagetoc.scrollTop = pageTocElement.offsetTop;
+                }
+                if (overflowBottom(pagetoc, pageTocElement) < 0) {
+                    pagetoc.scrollTop -= overflowBottom(pagetoc, pageTocElement);
+                }
+            }
+        }
+    }
+}
+
+if (document.getElementById("sidetoc") === null &&
+    document.getElementsByClassName("header").length > 0) {
+    // The sidetoc element doesn't exist yet, let's create it
+
+    // Create the empty sidetoc and pagetoc elements
+    const sidetoc = document.createElement("div");
+    const pagetoc = document.createElement("div");
+    sidetoc.id = "sidetoc";
+    pagetoc.id = "pagetoc";
+    sidetoc.appendChild(pagetoc);
+
+    // And append them to the current DOM
+    const main = document.querySelector('main');
+    main.insertBefore(sidetoc, main.firstChild);
+
+    // Populate sidebar on load
+    window.addEventListener("load", () => {
+        for (const header of document.getElementsByClassName("header")) {
+            const link = document.createElement("a");
+            link.innerHTML = header.innerHTML;
+            link.href = header.hash;
+            link.classList.add("pagetoc-" + header.parentElement.tagName);
+            document.getElementById("pagetoc").appendChild(link);
+            link.onclick = () => updatePageToc(link);
+        }
+        updatePageToc();
+    });
+
+    // Update page table of contents selected heading on scroll
+    window.addEventListener("scroll", () => updatePageToc());
+}