deploy: 0a1633ac3140c8be2e2eded5961aa2a17831328e

ayu-highlight.css

@@ -12,8 +12,7 @@ Original by Dempfi (https://github.com/dempfi/ayu)
 }
 
 .hljs-comment,
-.hljs-quote,
+.hljs-quote {
-.hljs-meta {
   color: #5c6773;
   font-style: italic;
 }
@@ -30,6 +29,7 @@ Original by Dempfi (https://github.com/dempfi/ayu)
 }
 
 .hljs-number,
+.hljs-meta,
 .hljs-builtin-name,
 .hljs-literal,
 .hljs-type,

book.js

@@ -408,7 +408,7 @@ function playpen_text(playpen) {
 (function sidebar() {
     var html = document.querySelector("html");
     var sidebar = document.getElementById("sidebar");
-    var sidebarScrollBox = document.getElementById("sidebar-scrollbox");
+    var sidebarScrollBox = document.querySelector(".sidebar-scrollbox");
     var sidebarLinks = document.querySelectorAll('#sidebar a');
     var sidebarToggleButton = document.getElementById("sidebar-toggle");
     var sidebarResizeHandle = document.getElementById("sidebar-resize-handle");
@@ -505,7 +505,7 @@ function playpen_text(playpen) {
     }, { passive: true });
 
     // Scroll sidebar to current active section
-    var activeSection = sidebar.querySelector(".active");
+    var activeSection = document.getElementById("sidebar").querySelector(".active");
     if (activeSection) {
         sidebarScrollBox.scrollTop = activeSection.offsetTop;
     }
@@ -580,26 +580,60 @@ function playpen_text(playpen) {
     });
 })();
 
-(function autoHideMenu() {
+(function controllMenu() {
     var menu = document.getElementById('menu-bar');
 
-    var previousScrollTop = document.scrollingElement.scrollTop;
+    (function controllPosition() {
-
+        var scrollTop = document.scrollingElement.scrollTop;
+        var prevScrollTop = scrollTop;
+        var minMenuY = -menu.clientHeight - 50;
+        // When the script loads, the page can be at any scroll (e.g. if you reforesh it).
+        menu.style.top = scrollTop + 'px';
+        // Same as parseInt(menu.style.top.slice(0, -2), but faster
+        var topCache = menu.style.top.slice(0, -2);
+        menu.classList.remove('sticky');
+        var stickyCache = false; // Same as menu.classList.contains('sticky'), but faster
         document.addEventListener('scroll', function () {
-        if (menu.classList.contains('folded') && document.scrollingElement.scrollTop < previousScrollTop) {
+            scrollTop = Math.max(document.scrollingElement.scrollTop, 0);
-            menu.classList.remove('folded');
+            // `null` means that it doesn't need to be updated
-        } else if (!menu.classList.contains('folded') && document.scrollingElement.scrollTop > previousScrollTop) {
+            var nextSticky = null;
-            menu.classList.add('folded');
+            var nextTop = null;
+            var scrollDown = scrollTop > prevScrollTop;
+            var menuPosAbsoluteY = topCache - scrollTop;
+            if (scrollDown) {
+                nextSticky = false;
+                if (menuPosAbsoluteY > 0) {
+                    nextTop = prevScrollTop;
                 }
-
+            } else {
-        if (!menu.classList.contains('bordered') && document.scrollingElement.scrollTop > 0) {
+                if (menuPosAbsoluteY > 0) {
-            menu.classList.add('bordered');
+                    nextSticky = true;
+                } else if (menuPosAbsoluteY < minMenuY) {
+                    nextTop = prevScrollTop + minMenuY;
                 }
-
-        if (menu.classList.contains('bordered') && document.scrollingElement.scrollTop === 0) {
-            menu.classList.remove('bordered');
             }
-
+            if (nextSticky === true && stickyCache === false) {
-        previousScrollTop = Math.max(document.scrollingElement.scrollTop, 0);
+                menu.classList.add('sticky');
+                stickyCache = true;
+            } else if (nextSticky === false && stickyCache === true) {
+                menu.classList.remove('sticky');
+                stickyCache = false;
+            }
+            if (nextTop !== null) {
+                menu.style.top = nextTop + 'px';
+                topCache = nextTop;
+            }
+            prevScrollTop = scrollTop;
         }, { passive: true });
     })();
+    (function controllBorder() {
+        menu.classList.remove('bordered');
+        document.addEventListener('scroll', function () {
+            if (menu.offsetTop === 0) {
+                menu.classList.remove('bordered');
+            } else {
+                menu.classList.add('bordered');
+            }
+        }, { passive: true });
+    })();
+})();

chapter_1.html

@@ -90,8 +90,8 @@
 
             <div class="page">
                 
-                <div id="menu-bar" class="menu-bar">
+                <div id="menu-bar-hover-placeholder"></div>
-                    <div id="menu-bar-sticky-container">
+                <div id="menu-bar" class="menu-bar sticky bordered">
                     <div class="left-buttons">
                         <button id="sidebar-toggle" class="icon-button" type="button" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
                             <i class="fa fa-bars"></i>
@@ -122,7 +122,6 @@
                         
                     </div>
                 </div>
-                </div>
 
                 
                 <div id="search-wrapper" class="hidden">

css/chrome.css

@@ -20,14 +20,13 @@ a > .hljs {
 
 /* Menu Bar */
 
-#menu-bar {
+#menu-bar,
-    position: -webkit-sticky;
+#menu-bar-hover-placeholder {
-    position: sticky;
-    top: 0;
     z-index: 101;
     margin: auto calc(0px - var(--page-padding));
 }
-#menu-bar > #menu-bar-sticky-container {
+#menu-bar {
+    position: relative;
     display: flex;
     flex-wrap: wrap;
     background-color: var(--bg);
@@ -35,10 +34,21 @@ a > .hljs {
     border-bottom-width: 1px;
     border-bottom-style: solid;
 }
-.js #menu-bar > #menu-bar-sticky-container {
+#menu-bar.sticky,
-    transition: transform 0.3s;
+.js #menu-bar-hover-placeholder:hover + #menu-bar,
+.js #menu-bar:hover,
+.js.sidebar-visible #menu-bar {
+    position: -webkit-sticky;
+    position: sticky;
+    top: 0 !important;
 }
-#menu-bar.bordered > #menu-bar-sticky-container  {
+#menu-bar-hover-placeholder {
+    position: sticky;
+    position: -webkit-sticky;
+    top: 0;
+    height: var(--menu-bar-height);
+}
+#menu-bar.bordered {
     border-bottom-color: var(--table-border-color);
 }
 #menu-bar i, #menu-bar .icon-button {
@@ -72,10 +82,6 @@ a > .hljs {
     text-decoration: none;
 }
 
-html:not(.sidebar-visible) #menu-bar:not(:hover).folded > #menu-bar-sticky-container {
-    transform: translateY(calc(-10px - var(--menu-bar-height)));
-}
-
 .left-buttons {
     display: flex;
     margin: 0 5px;
@@ -417,6 +423,11 @@ ul#searchresults span.teaser em {
     display: none;
 }
 
+.chapter li.expanded {
+    line-height: 1.5em;
+    margin-top: 0.6em;
+}
+
 .chapter li.expanded > a.toggle div {
     transform: rotate(90deg);
 }

css/general.css

@@ -60,6 +60,7 @@ h4 a.header:target {
 .page {
     outline: 0;
     padding: 0 var(--page-padding);
+    margin-top: calc(0px - var(--menu-bar-height)); /* Compensate for the #menu-bar-hover-placeholder */
 }
 .page-wrapper {
     box-sizing: border-box;
@@ -78,6 +79,9 @@ h4 a.header:target {
     margin-right: auto;
     max-width: var(--content-max-width);
 }
+.content p { line-height: 1.45em; }
+.content ol { line-height: 1.45em; }
+.content ul { line-height: 1.45em; }
 .content a { text-decoration: none; }
 .content a:hover { text-decoration: underline; }
 .content img { max-width: 100%; }

index.html

@@ -90,8 +90,8 @@
 
             <div class="page">
                 
-                <div id="menu-bar" class="menu-bar">
+                <div id="menu-bar-hover-placeholder"></div>
-                    <div id="menu-bar-sticky-container">
+                <div id="menu-bar" class="menu-bar sticky bordered">
                     <div class="left-buttons">
                         <button id="sidebar-toggle" class="icon-button" type="button" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
                             <i class="fa fa-bars"></i>
@@ -122,7 +122,6 @@
                         
                     </div>
                 </div>
-                </div>
 
                 
                 <div id="search-wrapper" class="hidden">

print.html

@@ -92,8 +92,8 @@
 
             <div class="page">
                 
-                <div id="menu-bar" class="menu-bar">
+                <div id="menu-bar-hover-placeholder"></div>
-                    <div id="menu-bar-sticky-container">
+                <div id="menu-bar" class="menu-bar sticky bordered">
                     <div class="left-buttons">
                         <button id="sidebar-toggle" class="icon-button" type="button" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
                             <i class="fa fa-bars"></i>
@@ -124,7 +124,6 @@
                         
                     </div>
                 </div>
-                </div>
 
                 
                 <div id="search-wrapper" class="hidden">