deploy: c8566191fcd7edf224db468f860c1b638fb8e763

4 files changed, 191 insertions, 0 deletions

diff --git a/v1.40/docs/website_files/indent-section-headers.css b/v1.40/docs/website_files/indent-section-headers.css
new file mode 100644
index 0000000000..f9b3c82ca6
--- /dev/null
+++ b/v1.40/docs/website_files/indent-section-headers.css
@@ -0,0 +1,7 @@
+/*
+ * Indents each chapter title in the left sidebar so that they aren't
+ * at the same level as the section headers.
+ */
+.chapter-item {
+    margin-left: 1em;
+}
\ No newline at end of file
diff --git a/v1.40/docs/website_files/remove-nav-buttons.css b/v1.40/docs/website_files/remove-nav-buttons.css
new file mode 100644
index 0000000000..4b280794ea
--- /dev/null
+++ b/v1.40/docs/website_files/remove-nav-buttons.css
@@ -0,0 +1,8 @@
+/* Remove the prev, next chapter buttons as they interfere with the
+ * table of contents.
+ * Note that the table of contents only appears on desktop, thus we
+ * only remove the desktop (wide) chapter buttons.
+ */
+.nav-wide-wrapper {
+    display: none
+}
\ No newline at end of file
diff --git a/v1.40/docs/website_files/table-of-contents.css b/v1.40/docs/website_files/table-of-contents.css
new file mode 100644
index 0000000000..d16bb3b988
--- /dev/null
+++ b/v1.40/docs/website_files/table-of-contents.css
@@ -0,0 +1,42 @@
+@media only screen and (max-width:1439px) {
+    .sidetoc {
+        display: none;
+    }
+}
+
+@media only screen and (min-width:1440px) {
+    main {
+        position: relative;
+        margin-left: 100px !important;
+    }
+    .sidetoc {
+        margin-left: auto;
+        margin-right: auto;
+        left: calc(100% + (var(--content-max-width))/4 - 140px);
+        position: absolute;
+        text-align: right;
+    }
+    .pagetoc {
+        position: fixed;
+        width: 250px;
+        overflow: auto;
+        right: 20px;
+        height: calc(100% - var(--menu-bar-height));
+    }
+    .pagetoc a {
+        color: var(--fg) !important;
+        display: block;
+        padding: 5px 15px 5px 10px;
+        text-align: left;
+        text-decoration: none;
+    }
+    .pagetoc a:hover,
+    .pagetoc a.active {
+        background: var(--sidebar-bg) !important;
+        color: var(--sidebar-fg) !important;
+    }
+    .pagetoc .active {
+        background: var(--sidebar-bg);
+        color: var(--sidebar-fg);
+    }
+}
diff --git a/v1.40/docs/website_files/table-of-contents.js b/v1.40/docs/website_files/table-of-contents.js
new file mode 100644
index 0000000000..0de5960b22
--- /dev/null
+++ b/v1.40/docs/website_files/table-of-contents.js
@@ -0,0 +1,134 @@
+const getPageToc = () => document.getElementsByClassName('pagetoc')[0];
+
+const pageToc = getPageToc();
+const pageTocChildren = [...pageToc.children];
+const headers = [...document.getElementsByClassName('header')];
+
+
+// Select highlighted item in ToC when clicking an item
+pageTocChildren.forEach(child => {
+    child.addEventHandler('click', () => {
+        pageTocChildren.forEach(child => {
+            child.classList.remove('active');
+        });
+        child.classList.add('active');
+    });
+});
+
+
+/**
+ * Test whether a node is in the viewport
+ */
+function isInViewport(node) {
+    const rect = node.getBoundingClientRect();
+    return rect.top >= 0 && rect.left >= 0 && rect.bottom <= (window.innerHeight || document.documentElement.clientHeight) && rect.right <= (window.innerWidth || document.documentElement.clientWidth);
+}
+
+
+/**
+ * Set a new ToC entry.
+ * Clear any previously highlighted ToC items, set the new one,
+ * and adjust the ToC scroll position.
+ */
+function setTocEntry() {
+    let activeEntry;
+    const pageTocChildren = [...getPageToc().children];
+
+    // Calculate which header is the current one at the top of screen
+    headers.forEach(header => {
+        if (window.pageYOffset >= header.offsetTop) {
+            activeEntry = header;
+        }
+    });
+
+    // Update selected item in ToC when scrolling
+    pageTocChildren.forEach(child => {
+        if (activeEntry.href.localeCompare(child.href) === 0) {
+            child.classList.add('active');
+        } else {
+            child.classList.remove('active');
+        }
+    });
+
+    let tocEntryForLocation = document.querySelector(`nav a[href="${activeEntry.href}"]`);
+    if (tocEntryForLocation) {
+        const headingForLocation = document.querySelector(activeEntry.hash);
+        if (headingForLocation && isInViewport(headingForLocation)) {
+            // Update ToC scroll
+            const nav = getPageToc();
+            const content = document.querySelector('html');
+            if (content.scrollTop !== 0) {
+                nav.scrollTo({
+                    top: tocEntryForLocation.offsetTop - 100,
+                    left: 0,
+                    behavior: 'smooth',
+                });
+            } else {
+                nav.scrollTop = 0;
+            }
+        }
+    }
+}
+
+
+/**
+ * Populate sidebar on load
+ */
+window.addEventListener('load', () => {
+    // Only create table of contents if there is more than one header on the page
+    if (headers.length <= 1) {
+        return;
+    }
+
+    // Create an entry in the page table of contents for each header in the document
+    headers.forEach((header, index) => {
+        const link = document.createElement('a');
+
+        // Indent shows hierarchy
+        let indent = '0px';
+        switch (header.parentElement.tagName) {
+            case 'H1':
+                indent = '5px';
+                break;
+            case 'H2':
+                indent = '20px';
+                break;
+            case 'H3':
+                indent = '30px';
+                break;
+            case 'H4':
+                indent = '40px';
+                break;
+            case 'H5':
+                indent = '50px';
+                break;
+            case 'H6':
+                indent = '60px';
+                break;
+            default:
+                break;
+        }
+
+        let tocEntry;
+        if (index == 0) {
+            // Create a bolded title for the first element
+            tocEntry = document.createElement("strong");
+            tocEntry.innerHTML = header.text;
+        } else {
+            // All other elements are non-bold
+            tocEntry = document.createTextNode(header.text);
+        }
+        link.appendChild(tocEntry);
+
+        link.style.paddingLeft = indent;
+        link.href = header.href;
+        pageToc.appendChild(link);
+    });
+    setTocEntry.call();
+});
+
+
+// Handle active headers on scroll, if there is more than one header on the page
+if (headers.length > 1) {
+    window.addEventListener('scroll', setTocEntry);
+}