collapsible pin pane

Author: peterzhangsnail

css/elements.css

@@ -569,7 +569,8 @@ tr.del > td {
   white-space: nowrap;
 }
 
-#menu-toc .item-toggle {
+#menu-toc .item-toggle,
+#menu-pins-header .item-toggle {
   display: inline-block;
   transform: rotate(-45deg) translate(-5px, -5px);
   transition: transform 0.1s ease;
@@ -593,15 +594,18 @@ tr.del > td {
   width: 20px;
 }
 
-#menu-toc li.active > .item-toggle {
+#menu-toc li.active > .item-toggle,
+#menu-pins-header.active > .item-toggle {
   transform: rotate(45deg) translate(-5px, -5px);
 }
 
-#menu-toc li > ol {
+#menu-toc li > ol,
+#menu-pins-header + #menu-pins-list {
   display: none;
 }
 
-#menu-toc li.active > ol {
+#menu-toc li.active > ol,
+#menu-pins-header.active + #menu-pins-list {
   display: block;
 }
 
@@ -668,10 +672,10 @@ tr.del > td {
   flex-grow: 0;
   flex-shrink: 0;
   width: 100%;
-  
+
   display: flex;
   flex-direction: column;
-  
+
   max-height: 300px;
 }
 

js/menu.js

@@ -238,7 +238,7 @@ function Menu() {
   document.addEventListener('keydown', this.documentKeydown.bind(this));
 
   // toc expansion
-  var tocItems = this.$menu.querySelectorAll('#menu-toc li');
+  var tocItems = this.$menu.querySelectorAll('#menu-toc li, #menu-pins .menu-pane-header');
   for (var i = 0; i < tocItems.length; i++) {
     var $item = tocItems[i];
     $item.addEventListener('click', function($item, event) {
@@ -848,3 +848,20 @@ document.addEventListener('DOMContentLoaded', function () {
   Toolbox.init();
   referencePane.init();
 })
+
+// collapsible pin pane
+document.addEventListener('DOMContentLoaded', collapsiblePinPane);
+
+function collapsiblePinPane() {
+  var MenuPins = document.getElementById('menu-pins');
+  var MenuPaneHeader = MenuPins.querySelector('.menu-pane-header');
+  MenuPaneHeader.setAttribute('id', 'menu-pins-header'); // Give the header an id for convenience.
+
+  var pinButton = document.createElement('span');
+  pinButton.textContent = "◢";
+  pinButton.setAttribute('class', 'item-toggle');
+  pinButton.style.cssFloat = 'right'; // Float the button to the right side, making it easier to be noticed.
+  pinButton.style.color = 'black'; // Set a different color for it, so the button won't be mixed with the background.
+
+  MenuPaneHeader.appendChild(pinButton);
+}