ScrollSpy for table of contents (#1557)

* ScrollSpy for table of contents

* Add reference

* Incorporate comments

* Simplify headingsCache and change ScrollSpy reference

* Add comment

* Fix lint errors

* Switch back to throlling, update comments

website/siteConfig.js

@@ -66,7 +66,10 @@ const siteConfig = {
 
     markdownPlugins: [require('./remarkableKatex'), require('./empty_thead')],
 
-    scripts: ['https://buttons.github.io/buttons.js'],
+    scripts: [
+        'https://buttons.github.io/buttons.js',
+        '/js/scrollspy.js',
+    ],
     stylesheets: ['https://cdn.jsdelivr.net/npm/katex@0.10.0-beta/dist/katex.min.css'],
 
     separateCss: ['static/static', 'static\\static'],

website/static/css/custom.css

@@ -1,3 +1,17 @@
+ul.toc-headings > li {
+    padding-bottom: 0px;   /* moved to li > a */
+}
+
+.toc-headings > li > a {
+    display: block;
+    padding: 4px;
+}
+
+.toc-headings > li > a.active {
+    background-color: rgba(27, 31, 35, 0.05);
+    font-weight: bold;
+}
+
 .fixedHeaderContainer header img {
     height: 80%;
 }

website/static/js/scrollspy.js

@@ -0,0 +1,46 @@
+// Inspired by ScrollSpy as in e.g. Bootstrap
+
+(function() {
+    const OFFSET = 10;
+    let timer;
+    let headingsCache;
+    const findHeadings = () => headingsCache ? headingsCache :
+        document.querySelectorAll('.toc-headings > li > a');
+    const onScroll = () => {
+        if (timer) {  // throttle
+            return;
+        }
+        timer = setTimeout(() => {
+            timer = null;
+            let found = false;
+            const headings = findHeadings();
+            for (let i = 0; i < headings.length; i++) {
+                // if !found and i is the last element, highlight the last
+                let current = !found;
+                if (!found && i < headings.length - 1) {
+                    const next = headings[i + 1].href.split('#')[1];
+                    const nextHeader = document.getElementById(next);
+                    const top = nextHeader.getBoundingClientRect().top;
+                    // The following tests whether top + scrollTop
+                    // (the top of the header) is greater than scrollTop
+                    // (where scrollTop = window.pageYOffset, the top of
+                    // the window), with OFFSET pixels of slop.
+                    current = top > OFFSET;
+                }
+                if (current) {
+                    found = true;
+                    headings[i].className = "active";
+                } else {
+                    headings[i].className = "";
+                }
+            }
+        }, 100);
+    };
+    document.addEventListener('scroll', onScroll);
+    document.addEventListener('resize', onScroll);
+    document.addEventListener('DOMContentLoaded', () => {
+        // Cache the headings once the page has fully loaded.
+        headingsCache = findHeadings();
+        onScroll();
+    });
+})();