diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index dcf51d0..82d3a26 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -82,18 +82,23 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
let json := Json.arr declList
- FS.writeFile (basePath / "searchable_data.bmp") json.compress
FS.writeFile (basePath / "index.html") indexHtml.toString
- FS.writeFile (basePath / "style.css") styleCss
FS.writeFile (basePath / "404.html") notFoundHtml.toString
+ FS.writeFile (basePath / "find" / "index.html") findHtml.toString
+
+ FS.writeFile (basePath / "style.css") styleCss
+
+ let declarationDataPath := basePath / "declaration-data.bmp"
+ FS.writeFile declarationDataPath json.compress
+ FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec
+
+ FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" config.root)
+ FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs
FS.writeFile (basePath / "nav.js") navJs
+ FS.writeFile (basePath / "find" / "find.js") findJs
+ FS.writeFile (basePath / "how-about.js") howAboutJs
FS.writeFile (basePath / "search.js") searchJs
FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs
- FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" config.root)
-
- FS.writeFile (basePath / "find" / "index.html") findHtml.toString
- FS.writeFile (basePath / "find" / "find.js") findJs
-
for (module, content) in result.moduleInfo.toArray do
let moduleHtml := ReaderT.run (moduleToHtml content) config
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 0188511..20443f8 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -48,7 +48,9 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
section Static
def styleCss : String := include_str "./static/style.css"
def siteRootJs : String := include_str "./static/site-root.js"
+ def declarationDataCenterJs : String := include_str "./static/declaration-data.js"
def navJs : String := include_str "./static/nav.js"
+ def howAboutJs : String := include_str "./static/how-about.js"
def searchJs : String := include_str "./static/search.js"
def findJs : String := include_str "./static/find/find.js"
def mathjaxConfigJs : String := include_str "./static/mathjax-config.js"
diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean
index 60e56ac..95bbd8e 100644
--- a/DocGen4/Output/Find.lean
+++ b/DocGen4/Output/Find.lean
@@ -10,7 +10,7 @@ def find : HtmlM Html := do
pure
-
+
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index d4f358f..05390fe 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -24,13 +24,15 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
-
+
+
+
diff --git a/static/declaration-data.js b/static/declaration-data.js
new file mode 100644
index 0000000..ec72aa8
--- /dev/null
+++ b/static/declaration-data.js
@@ -0,0 +1,127 @@
+/**
+ * This module is a wrapper that facilitates manipulating the declaration data.
+ *
+ * Please see {@link DeclarationDataCenter} for more information.
+ */
+
+import { SITE_ROOT } from "./site-root.js";
+
+/**
+ * The DeclarationDataCenter is used for declaration searching.
+ *
+ * For usage, see the {@link init} and {@link search} methods.
+ */
+export class DeclarationDataCenter {
+ /**
+ * The declaration data. Users should not interact directly with this field.
+ *
+ * *NOTE:* This is not made private to support legacy browsers.
+ */
+ declarationData = [];
+
+ /**
+ * Used to implement the singleton, in case we need to fetch data mutiple times in the same page.
+ */
+ static singleton = null;
+
+ /**
+ * Construct a DeclarationDataCenter with given data.
+ *
+ * Please use {@link DeclarationDataCenter.init} instead, which automates the data fetching process.
+ * @param {*} declarationData
+ */
+ constructor(declarationData) {
+ this.declarationData = declarationData;
+ }
+
+ /**
+ * The actual constructor of DeclarationDataCenter
+ * @returns {Promise}
+ */
+ static async init() {
+ if (!DeclarationDataCenter.singleton) {
+ const dataUrl = new URL(
+ `${SITE_ROOT}declaration-data.bmp`,
+ window.location
+ );
+ const response = await fetch(dataUrl);
+ const json = await response.json();
+ const data = json.map(({ name, description, link, source }) => [
+ name,
+ name.toLowerCase(),
+ description.toLowerCase(),
+ link,
+ source,
+ ]);
+ DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
+ }
+ return DeclarationDataCenter.singleton;
+ }
+
+ /**
+ * Search for a declaration.
+ * @returns {Array}
+ */
+ search(pattern, strict = false) {
+ if (!pattern) {
+ return [];
+ }
+ // TODO: implement strict
+ return getMatches(this.declarationData, pattern);
+ }
+}
+
+function isSeparater(char) {
+ return char === "." || char === "_";
+}
+
+function matchCaseSensitive(
+ declName,
+ lowerDeclName,
+ pattern
+) {
+ let i = 0,
+ j = 0,
+ err = 0,
+ lastMatch = 0;
+ while (i < declName.length && j < pattern.length) {
+ if (
+ pattern[j] === declName[i] ||
+ pattern[j] === lowerDeclName[i]
+ ) {
+ err += (isSeparater(pattern[j]) ? 0.125 : 1) * (i - lastMatch);
+ if (pattern[j] !== declName[i]) err += 0.5;
+ lastMatch = i + 1;
+ j++;
+ } else if (isSeparater(declName[i])) {
+ err += 0.125 * (i + 1 - lastMatch);
+ lastMatch = i + 1;
+ }
+ i++;
+ }
+ err += 0.125 * (declName.length - lastMatch);
+ if (j === pattern.length) {
+ return err;
+ }
+}
+
+function getMatches(declarations, pattern, maxResults = 30) {
+ const lowerPats = pattern.toLowerCase().split(/\s/g);
+ const patNoSpaces = pattern.replace(/\s/g, "");
+ const results = [];
+ for (const [decl, lowerDecl, lowerDoc, link, source] of declarations) {
+ let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces);
+ // match all words as substrings of docstring
+ if (
+ !(err < 3) &&
+ pattern.length > 3 &&
+ lowerPats.every((l) => lowerDoc.indexOf(l) != -1)
+ ) {
+ err = 3;
+ }
+ if (err !== undefined) {
+ results.push({ decl, err, link, source });
+ }
+ }
+ return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults);
+}
diff --git a/static/find/find.js b/static/find/find.js
index 480f725..7fcb9ec 100644
--- a/static/find/find.js
+++ b/static/find/find.js
@@ -1,22 +1,28 @@
-import { SITE_ROOT } from "../site-root.js";
-import { declSearch } from "../search.js";
+/**
+ * This module is used for the `/find` endpoint.
+ */
-async function findRedirect(query, isSource) {
- return declSearch(query).then((results) => {
- window.location.replace(isSource? results[0].source : results[0].link);
- }).catch(() => {
+import { SITE_ROOT } from "../site-root.js";
+import { DeclarationDataCenter } from "../declaration-data.js";
+
+async function findRedirect(pattern, isSource) {
+ const dataCenter = await DeclarationDataCenter.init();
+ try {
+ let results = dataCenter.search(pattern);
+ window.location.replace(isSource ? results[0].source : results[0].link);
+ } catch {
window.location.replace(`${SITE_ROOT}404.html`);
- });
+ }
}
-let splits = window.location.href.split("#");
+let hash = window.location.hash.split("#");
-if (splits.length < 2) {
+if (hash.length == 0) {
window.location.replace(`${SITE_ROOT}/404.html`);
}
-if (splits[1].endsWith("/src")) {
- findRedirect(splits[1].replace("/src", ""), true);
+if (hash[1].endsWith("/src")) {
+ findRedirect(hash.replace("/src", ""), true);
} else {
- findRedirect(splits[1], false);
+ findRedirect(hash, false);
}
diff --git a/static/how-about.js b/static/how-about.js
new file mode 100644
index 0000000..421f6e4
--- /dev/null
+++ b/static/how-about.js
@@ -0,0 +1,35 @@
+/**
+ * This module implements the `howabout` functionality in the 404 page.
+ */
+
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+const HOW_ABOUT = document.querySelector("#howabout");
+
+if (HOW_ABOUT) {
+ HOW_ABOUT.innerText = "Please wait a second. I'll try to help you.";
+
+ HOW_ABOUT.parentNode
+ .insertBefore(document.createElement("pre"), HOW_ABOUT)
+ .appendChild(document.createElement("code")).innerText =
+ window.location.href.replace(/[/]/g, "/\u200b");
+
+ // TODO: add how about functionality for similar page as well.
+ const pattern = window.location.hash.replace("#", "");
+
+ DeclarationDataCenter.init().then((dataCenter) => {
+ let results = dataCenter.search(pattern);
+ if (results.length > 0) {
+ HOW_ABOUT.innerText = "How about one of these instead:";
+ const ul = HOW_ABOUT.appendChild(document.createElement("ul"));
+ for (const { decl, link } of results) {
+ const li = ul.appendChild(document.createElement("li"));
+ const a = li.appendChild(document.createElement("a"));
+ a.href = link;
+ a.appendChild(document.createElement("code")).innerText = decl;
+ }
+ } else {
+ HOW_ABOUT.innerText = "Sorry, I cannot find any similar declarations. Check the link or use the module navigation to find what you want :P";
+ }
+ });
+}
diff --git a/static/mathjax-config.js b/static/mathjax-config.js
index 9e470bc..076dbf6 100644
--- a/static/mathjax-config.js
+++ b/static/mathjax-config.js
@@ -1,26 +1,41 @@
/*
- * This file is for configing MathJax behavior.
- * Seehttps://docs.mathjax.org/en/latest/web/configuration.html
- */
-
-/**
+ * This file is for configing MathJax behavior.
+ * See https://docs.mathjax.org/en/latest/web/configuration.html
+ *
* This configuration is copied from old doc-gen3
* https://github.com/leanprover-community/doc-gen
*/
MathJax = {
tex: {
- inlineMath: [['$', '$']],
- displayMath: [['$$', '$$']]
+ inlineMath: [["$", "$"]],
+ displayMath: [["$$", "$$"]],
},
options: {
skipHtmlTags: [
- 'script', 'noscript', 'style', 'textarea', 'pre',
- 'code', 'annotation', 'annotation-xml',
- 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name',
- 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields',
- 'constructor', 'constructors', 'instances'
+ "script",
+ "noscript",
+ "style",
+ "textarea",
+ "pre",
+ "code",
+ "annotation",
+ "annotation-xml",
+ "decl",
+ "decl_meta",
+ "attributes",
+ "decl_args",
+ "decl_header",
+ "decl_name",
+ "decl_type",
+ "equation",
+ "equations",
+ "structure_field",
+ "structure_fields",
+ "constructor",
+ "constructors",
+ "instances",
],
- ignoreHtmlClass: 'tex2jax_ignore',
- processHtmlClass: 'tex2jax_process',
+ ignoreHtmlClass: "tex2jax_ignore",
+ processHtmlClass: "tex2jax_process",
},
-};
\ No newline at end of file
+};
diff --git a/static/nav.js b/static/nav.js
index 3889da3..ff8404e 100644
--- a/static/nav.js
+++ b/static/nav.js
@@ -1,232 +1,43 @@
-import { declSearch } from "./search.js";
-
-// Persistent expansion cookie for the file tree
-// ---------------------------------------------
+/**
+ * This module is used to implement persistent navbar expansion.
+ */
+// The variable to store the expansion information.
let expanded = {};
-for (const e of (sessionStorage.getItem('expanded') || '').split(',')) {
- if (e !== '') {
+
+// Load expansion information from sessionStorage.
+for (const e of (sessionStorage.getItem("expanded") || "").split(",")) {
+ if (e !== "") {
expanded[e] = true;
}
}
+/**
+ * Save expansion information to sessionStorage.
+ */
function saveExpanded() {
- sessionStorage.setItem("expanded",
- Object.getOwnPropertyNames(expanded).filter((e) => expanded[e]).join(","));
+ sessionStorage.setItem(
+ "expanded",
+ Object.getOwnPropertyNames(expanded)
+ .filter((e) => expanded[e])
+ .join(",")
+ );
}
-for (const elem of document.getElementsByClassName('nav_sect')) {
- const id = elem.getAttribute('data-path');
+// save expansion information when user change the expansion.
+for (const elem of document.getElementsByClassName("nav_sect")) {
+ const id = elem.getAttribute("data-path");
if (!id) continue;
if (expanded[id]) {
elem.open = true;
}
- elem.addEventListener('toggle', () => {
+ elem.addEventListener("toggle", () => {
expanded[id] = elem.open;
saveExpanded();
});
}
-for (const currentFileLink of document.getElementsByClassName('visible')) {
- currentFileLink.scrollIntoView({block: 'center'});
-}
-
-
-
-
-
-
-// Tactic list tag filter
-// ----------------------
-
-function filterSelectionClass(tagNames, classname) {
- if (tagNames.length == 0) {
- for (const elem of document.getElementsByClassName(classname)) {
- elem.classList.remove("hide");
- }
- } else {
- // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
- for (const elem of document.getElementsByClassName(classname)) {
- elem.classList.add("hide");
- for (const tagName of tagNames) {
- if (elem.classList.contains(tagName)) {
- elem.classList.remove("hide");
- }
- }
- }
- }
- }
-
- function filterSelection(c) {
- filterSelectionClass(c, "tactic");
- filterSelectionClass(c, "taclink");
- }
-
-var filterBoxes = document.getElementsByClassName("tagfilter");
-
-function updateDisplay() {
- filterSelection(getSelectValues());
-}
-
-function getSelectValues() {
- var result = [];
-
- for (const opt of filterBoxes) {
-
- if (opt.checked) {
- result.push(opt.value);
- }
- }
- return result;
- }
-
-function setSelectVal(val) {
- for (const opt of filterBoxes) {
- opt.checked = val;
- }
-}
-
-updateDisplay();
-
-for (const opt of filterBoxes) {
- opt.addEventListener('change', updateDisplay);
-}
-
-const tse = document.getElementById("tagfilter-selectall")
-if (tse != null) {
- tse.addEventListener('change', function() {
- setSelectVal(this.checked);
- updateDisplay();
- });
-}
-
-
-
-
-
-
-// Simple declaration search
-// -------------------------
-
-const srId = 'search_results';
-document.getElementById('search_form')
- .appendChild(document.createElement('div'))
- .id = srId;
-
-function handleSearchCursorUpDown(down) {
- const sel = document.querySelector(`#${srId} .selected`);
- const sr = document.getElementById(srId);
- if (sel) {
- sel.classList.remove('selected');
- const toSelect = down ?
- sel.nextSibling || sr.firstChild:
- sel.previousSibling || sr.lastChild;
- toSelect && toSelect.classList.add('selected');
- } else {
- const toSelect = down ? sr.firstChild : sr.lastChild;
- toSelect && toSelect.classList.add('selected');
- }
-}
-
-function handleSearchEnter() {
- const sel = document.querySelector(`#${srId} .selected`)
- || document.getElementById(srId).firstChild;
- sel.click();
-}
-
-const searchInput = document.querySelector('#search_form input[name=q]');
-
-searchInput.addEventListener('keydown', (ev) => {
- switch (ev.key) {
- case 'Down':
- case 'ArrowDown':
- ev.preventDefault();
- handleSearchCursorUpDown(true);
- break;
- case 'Up':
- case 'ArrowUp':
- ev.preventDefault();
- handleSearchCursorUpDown(false);
- break;
- case 'Enter':
- ev.preventDefault();
- handleSearchEnter();
- break;
- }
-});
-
-searchInput.addEventListener('input', async (ev) => {
- const text = ev.target.value;
-
- if (!text) {
- const sr = document.getElementById(srId);
- sr.removeAttribute('state');
- sr.replaceWith(sr.cloneNode(false));
- return;
- }
-
- document.getElementById(srId).setAttribute('state', 'loading');
-
- const result = await declSearch(text);
- if (ev.target.value != text) return;
-
- const oldSR = document.getElementById('search_results');
- const sr = oldSR.cloneNode(false);
- for (const {decl, link} of result) {
- const d = sr.appendChild(document.createElement('a'));
- d.innerText = decl;
- d.title = decl;
- d.href = link;
- }
- sr.setAttribute('state', 'done');
- oldSR.replaceWith(sr);
-});
-
-
-
-
-
-
-// 404 page goodies
-// ----------------
-
-const howabout = document.getElementById('howabout');
-if (howabout) {
- howabout.innerText = "Please wait a second. I'll try to help you.";
-
- howabout.parentNode
- .insertBefore(document.createElement('pre'), howabout)
- .appendChild(document.createElement('code'))
- .innerText = window.location.href.replace(/[/]/g, '/\u200b');
-
- const query = window.location.href.match(/[/]([^/]+)(?:\.html|[/])?$/)[1];
- declSearch(query).then((results) => {
- howabout.innerText = 'How about one of these instead:';
- const ul = howabout.appendChild(document.createElement('ul'));
- for (const {decl, link} of results) {
- const li = ul.appendChild(document.createElement('li'));
- const a = li.appendChild(document.createElement('a'));
- a.href = link;
- a.appendChild(document.createElement('code')).innerText = decl;
- }
- });
-}
-
-
-
-
-
-
-// Rewrite GitHub links
-// --------------------
-
-for (const elem of document.getElementsByClassName('gh_link')) {
- const a = elem.firstElementChild;
- // commit is set in add_commit.js
- for (const [prefix, replacement] of commit) {
- if (a.href.startsWith(prefix)) {
- a.href = a.href.replace(prefix, replacement);
- break;
- }
- }
-}
+// Scroll to center.
+for (const currentFileLink of document.getElementsByClassName("visible")) {
+ currentFileLink.scrollIntoView({ block: "center" });
+}
\ No newline at end of file
diff --git a/static/search.js b/static/search.js
index 3449036..a6a72ea 100644
--- a/static/search.js
+++ b/static/search.js
@@ -1,67 +1,104 @@
-import { SITE_ROOT } from "./site-root.js";
+/**
+ * This module is used to handle user's interaction with the search form.
+ */
-function isSep(c) {
- return c === '.' || c === '_';
-}
+import { DeclarationDataCenter } from "./declaration-data.js";
-function matchCaseSensitive(declName, lowerDeclName, pat) {
- let i = 0, j = 0, err = 0, lastMatch = 0
- while (i < declName.length && j < pat.length) {
- if (pat[j] === declName[i] || pat[j] === lowerDeclName[i]) {
- err += (isSep(pat[j]) ? 0.125 : 1) * (i - lastMatch);
- if (pat[j] !== declName[i]) err += 0.5;
- lastMatch = i + 1;
- j++;
- } else if (isSep(declName[i])) {
- err += 0.125 * (i + 1 - lastMatch);
- lastMatch = i + 1;
- }
- i++;
- }
- err += 0.125 * (declName.length - lastMatch);
- if (j === pat.length) {
- return err;
- }
-}
-export function loadDecls(searchableDataCnt) {
- return searchableDataCnt.map(({name, description, link, source}) => [name, name.toLowerCase(), description.toLowerCase(), link, source]);
-}
+const SEARCH_FORM = document.querySelector("#search_form");
+const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]");
-export function getMatches(decls, pat, maxResults = 30) {
- const lowerPats = pat.toLowerCase().split(/\s/g);
- const patNoSpaces = pat.replace(/\s/g, '');
- const results = [];
- for (const [decl, lowerDecl, lowerDoc, link, source] of decls) {
- let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces);
+// Create an `div#search_results` to hold all search results.
+let sr = document.createElement("div");
+sr.id = "search_results";
+SEARCH_FORM.appendChild(sr);
- // match all words as substrings of docstring
- if (!(err < 3) && pat.length > 3 && lowerPats.every(l => lowerDoc.indexOf(l) != -1)) {
- err = 3;
- }
-
- if (err !== undefined) {
- results.push({decl, err, link, source});
- }
- }
- return results.sort(({err: a}, {err: b}) => a - b).slice(0, maxResults);
-}
-
-const declURL = new URL(`${SITE_ROOT}searchable_data.bmp`, window.location);
-
-export const getDecls = (() => {
- let decls;
- return () => {
- if (!decls) decls = new Promise((resolve, reject) => {
- const req = new XMLHttpRequest();
- req.responseType = 'json';
- req.addEventListener('load', () => resolve(loadDecls(req.response)));
- req.addEventListener('error', () => reject());
- req.open('GET', declURL);
- req.send();
- })
- return decls;
+/**
+ * Attach `selected` class to the the selected search result.
+ */
+function handleSearchCursorUpDown(down) {
+ const sel = sr.querySelector(`.selected`);
+ if (sel) {
+ sel.classList.remove("selected");
+ const toSelect = down
+ ? sel.nextSibling || sr.firstChild
+ : sel.previousSibling || sr.lastChild;
+ toSelect && toSelect.classList.add("selected");
+ } else {
+ const toSelect = down ? sr.firstChild : sr.lastChild;
+ toSelect && toSelect.classList.add("selected");
}
-})()
+}
-export const declSearch = async (q) => getMatches(await getDecls(), q);
\ No newline at end of file
+/**
+ * Perform search (when enter is pressed).
+ */
+function handleSearchEnter() {
+ const sel =
+ sr.querySelector(`.selected`) ||
+ sr.firstChild;
+ sel.click();
+}
+
+/**
+ * Allow user to navigate search results with up/down arrow keys, and choose with enter.
+ */
+SEARCH_INPUT.addEventListener("keydown", (ev) => {
+ switch (ev.key) {
+ case "Down":
+ case "ArrowDown":
+ ev.preventDefault();
+ handleSearchCursorUpDown(true);
+ break;
+ case "Up":
+ case "ArrowUp":
+ ev.preventDefault();
+ handleSearchCursorUpDown(false);
+ break;
+ case "Enter":
+ ev.preventDefault();
+ handleSearchEnter();
+ break;
+ }
+});
+
+/**
+ * Remove all children of a DOM node.
+ */
+function removeAllChildren(node) {
+ while (node.firstChild) {
+ node.removeChild(node.lastChild);
+ }
+}
+
+/**
+ * Search autocompletion.
+ */
+SEARCH_INPUT.addEventListener("input", async (ev) => {
+ const text = ev.target.value;
+
+ // If no input clear all.
+ if (!text) {
+ sr.removeAttribute("state");
+ removeAllChildren(sr);
+ return;
+ }
+
+ // searching
+ sr.setAttribute("state", "loading");
+ const dataCenter = await DeclarationDataCenter.init();
+ const result = dataCenter.search(text);
+
+ // in case user has updated the input.
+ if (ev.target.value != text) return;
+
+ // update search results
+ removeAllChildren(sr);
+ for (const { decl, link } of result) {
+ const d = sr.appendChild(document.createElement("a"));
+ d.innerText = decl;
+ d.title = decl;
+ d.href = link;
+ }
+ sr.setAttribute("state", "done");
+});
diff --git a/static/site-root.js b/static/site-root.js
index 0663d6b..3dd39a3 100644
--- a/static/site-root.js
+++ b/static/site-root.js
@@ -1 +1,4 @@
+/**
+ * Get the site root, {siteRoot} is to be replaced by doc-gen4.
+ */
export const SITE_ROOT = "{siteRoot}";
\ No newline at end of file
diff --git a/static/tactic.js b/static/tactic.js
new file mode 100644
index 0000000..e40c4ec
--- /dev/null
+++ b/static/tactic.js
@@ -0,0 +1,61 @@
+// TODO: The tactic part seem to be unimplemented now.
+
+function filterSelectionClass(tagNames, classname) {
+ if (tagNames.length == 0) {
+ for (const elem of document.getElementsByClassName(classname)) {
+ elem.classList.remove("hide");
+ }
+ } else {
+ // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
+ for (const elem of document.getElementsByClassName(classname)) {
+ elem.classList.add("hide");
+ for (const tagName of tagNames) {
+ if (elem.classList.contains(tagName)) {
+ elem.classList.remove("hide");
+ }
+ }
+ }
+ }
+}
+
+function filterSelection(c) {
+ filterSelectionClass(c, "tactic");
+ filterSelectionClass(c, "taclink");
+}
+
+var filterBoxes = document.getElementsByClassName("tagfilter");
+
+function updateDisplay() {
+ filterSelection(getSelectValues());
+}
+
+function getSelectValues() {
+ var result = [];
+
+ for (const opt of filterBoxes) {
+ if (opt.checked) {
+ result.push(opt.value);
+ }
+ }
+ return result;
+}
+
+function setSelectVal(val) {
+ for (const opt of filterBoxes) {
+ opt.checked = val;
+ }
+}
+
+updateDisplay();
+
+for (const opt of filterBoxes) {
+ opt.addEventListener("change", updateDisplay);
+}
+
+const tse = document.getElementById("tagfilter-selectall");
+if (tse != null) {
+ tse.addEventListener("change", function () {
+ setSelectVal(this.checked);
+ updateDisplay();
+ });
+}