diff --git a/docs/manual.nix b/docs/manual.nix index 113fb78..4becdf2 100644 --- a/docs/manual.nix +++ b/docs/manual.nix @@ -62,7 +62,8 @@ in # Copy anchor scripts to the script directory in document root. cp -vt "$dest"/script \ ${./static/script}/anchor-min.js \ - ${./static/script}/anchor-use.js + ${./static/script}/anchor-use.js \ + ${./static/script}/search.js substituteInPlace ./options.md \ --subst-var-by OPTIONS_JSON ./config-options.json @@ -100,6 +101,7 @@ in --script highlightjs/loader.js \ --script script/anchor-use.js \ --script script/anchor-min.js \ + --script script/search.js \ --toc-depth 2 \ --section-toc-depth 1 \ manual.md \ diff --git a/docs/static/script/search.js b/docs/static/script/search.js new file mode 100644 index 0000000..618ec4a --- /dev/null +++ b/docs/static/script/search.js @@ -0,0 +1,39 @@ +document.addEventListener("DOMContentLoaded", () => { + // The search widget should only be visible if we're in the options page. Else, we + // want it hidden. + if (window.location.pathname.endsWith("options.html")) { + const searchBar = document.createElement("div"); + searchBar.id = "search-bar"; + searchBar.innerHTML = ` + +
+ `; + + document.body.prepend(searchBar); + + const dtElements = document.querySelectorAll("dt"); + const ddElements = document.querySelectorAll("dd"); + + if (dtElements.length === 0 || ddElements.length === 0) { + console.warn( + "No