[docs] replace AnchorJS with custom script

use it in rendered .rst documents as well as in .md ones
5 months ago · 6dac43ad60
parent 141a93c8fd
commit 6dac43ad60
2 changed files with 46 additions and 3 deletions
--- a/docs/_layouts/default.html
+++ b/docs/_layouts/default.html
@ -1,5 +1,5 @@
 <!DOCTYPE html>
-<html lang="{{ page.lang | default: site.lang | default: "en-US" }}">
+<html lang="en-US">
  <head>
    <meta charset="UTF-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
@ -8,6 +8,7 @@
 {% seo %}
    <link rel="stylesheet" href="{{ "/assets/css/style.css?v=" | append: site.github.build_revision | relative_url }}">
    <script src="links.js"></script>
  </head>
  <body>
    <div class="container-lg px-3 my-5 markdown-body">
@ -15,7 +16,5 @@
      {{ content }}
    </div>
    <script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.1.0/anchor.min.js" integrity="sha256-lZaRhKri35AyJSypXXs4o6OPFTbTmUoltBbDCbdzegg=" crossorigin="anonymous"></script>
    <script>anchors.add();</script>
  </body>
 </html>
--- a/docs/links.js
+++ b/docs/links.js
@ -0,0 +1,44 @@
 "use strict";
 function add_header_links()
 {
    let style = document.createElement("style");
    style.id = "headerlinks"
    document.head.appendChild(style);
    style.sheet.insertRule(
        "a.headerlink {"           +
        "  visibility: hidden;"    +
        "  text-decoration: none;" +
        "  font-size: 0.8em;"      +
        "  padding: 0 4px 0 4px;"  +
        "}");
    style.sheet.insertRule(
        ":hover > a.headerlink {"  +
        "  visibility: visible;"   +
        "}");
    let headers = document.querySelectorAll("h2, h3, h4, h5, h6");
    for (let i = 0, len = headers.length; i < len; ++i)
    {
        let header = headers[i];
        let id = header.id || header.parentNode.id;
        if (!id)
            continue;
        let link = document.createElement("a");
        link.href = "#" + id;
        link.className = "headerlink";
        link.textContent = "¶";
        header.appendChild(link);
    }
 }
 if (document.readyState !== "loading") {
    add_header_links();
 } else {
    document.addEventListener("DOMContentLoaded", add_header_links);
 }