doc: use AnchorJS to add visible anchor links on headings.

The standard library gets some extra attention here, to put anchor links
onto each of the entries individually.

Author: johnbartholomew

doc/_layouts/base.html

@@ -20,6 +20,7 @@
     });
     </script>
     <script type="text/javascript" src="/third_party/MathJax-2.7.2/MathJax.js"></script>
+    <script type="text/javascript" src="/third_party/anchor.min.js"></script>
 
 
     <!-- Google Analytics -->
@@ -134,6 +135,14 @@
   </div>
 </div>
 
+<script>
+  anchors.options = {
+    placement: 'right',
+    visible: 'always',
+    icon: '#'
+  };
+  anchors.add('h2,h3');
+</script>
 </body>
 
 </html>

doc/_layouts/stdlib.html

@@ -0,0 +1,14 @@
+---
+layout: base
+viewport_width: 576
+---
+{{ content }}
+
+<script>
+(function(){
+  let funcAnchors = new AnchorJS({
+    placement: 'left',
+  });
+  funcAnchors.add('h4');
+})(window);
+</script>

doc/_stdlib_gen/stdlib.jsonnet

@@ -84,7 +84,7 @@ local stdlibPage = [
 ];
 
 local stdlibFrontMatter = {
-  layout: 'default',
+  layout: 'stdlib',
   title: 'Standard Library',
 };
 

doc/ref/stdlib.html

@@ -1,6 +1,6 @@
 ---
 # AUTOGENERATED FILE. DO NOT EDIT BY HAND!
-layout: default
+layout: stdlib
 title: Standard Library
 ---