From 6dac43ad60c977cfa39eb402601c99fa8457b951 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mike=20F=C3=A4hrmann?= Date: Sat, 13 Apr 2024 17:53:04 +0200 Subject: [PATCH] [docs] replace AnchorJS with custom script use it in rendered .rst documents as well as in .md ones --- docs/_layouts/default.html | 5 ++--- docs/links.js | 44 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 46 insertions(+), 3 deletions(-) create mode 100644 docs/links.js diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html index 955164a3..8658aefa 100644 --- a/docs/_layouts/default.html +++ b/docs/_layouts/default.html @@ -1,5 +1,5 @@ - + @@ -8,6 +8,7 @@ {% seo %} +
@@ -15,7 +16,5 @@ {{ content }}
- - diff --git a/docs/links.js b/docs/links.js new file mode 100644 index 00000000..487907b9 --- /dev/null +++ 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); +}