+ pure
@@ -29,7 +29,12 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
pure
- {Html.element "summary" true #[] #[{h.getName.toString}]}
+ {
+ if (←getResult).moduleInfo.contains h.getName then
+ Html.element "summary" true #[] #[{h.getName.toString}]
+ else
+ {h.getName.toString}
+ }
[dirNodes]
[fileNodes]
diff --git a/DocGen4/Output/Semantic.lean b/DocGen4/Output/Semantic.lean
new file mode 100644
index 0000000..7b22cdf
--- /dev/null
+++ b/DocGen4/Output/Semantic.lean
@@ -0,0 +1,58 @@
+import DocGen4.Output.Template
+import DocGen4.Output.DocString
+import Lean.Data.Xml
+
+open Lean Xml
+
+namespace DocGen4
+namespace Output
+
+instance : ToString $ Array Element where
+ toString xs := xs.map toString |>.foldl String.append ""
+
+instance : Coe Element Content where
+ coe e := Content.Element e
+
+-- TODO: syntax metaprogramming and basic semantic data
+
+def semanticXml (i : DocInfo) : HtmlM $ Array Element := do
+ pure #[
+ Element.Element
+ "rdf:RDF"
+ (Std.RBMap.fromList [
+ ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"),
+ ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#")
+ ] _)
+ #[
+ Element.Element
+ "rdf:Description"
+ (Std.RBMap.fromList [
+ ("rdf:about", s!"{←getRoot}semactic/{i.getName.hash}.xml#")
+ ] _)
+ #[]
+ ]
+ ]
+
+def schemaXml : HtmlM $ Array Element := do
+ pure #[
+ Element.Element
+ "rdf:RDF"
+ (Std.RBMap.fromList [
+ ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"),
+ ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#")
+ ] _)
+ #[
+ Element.Element
+ "docgen4:hasInstance"
+ Std.RBMap.empty
+ #[
+ Element.Element
+ "rdfs:type"
+ Std.RBMap.empty
+ #[Content.Character "rdf:Property"]
+ ]
+ ]
+ ]
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index 8ed58ee..05390fe 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -15,46 +15,48 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
pure
+
+
{title}
+
+
+
+
-
{title}
-
-
+
+
+
+
+
+
+
+
+
+
-
+
-
- Documentation
- {title}
- -- TODO: Replace this form with our own search
-
-
+
+ Documentation
+ {title}
+ -- TODO: Replace this form with our own search
+
+
- [site]
-
- {←navbar}
+ [site]
+
+ {←navbar}
- -- Lean in JS in HTML in Lean...very meta
-
-
- -- TODO Add more js stuff
-
-
- -- mathjax
-
-
-
+
diff --git a/Main.lean b/Main.lean
index 062cf6b..88a0640 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,15 +1,30 @@
import DocGen4
import Lean
+import Cli
-open DocGen4 Lean IO
+open DocGen4 Lean Cli
-def main (modules : List String) : IO Unit := do
- if modules.isEmpty then
- IO.println "Usage: doc-gen4 Module1 Module2 ..."
- IO.Process.exit 1
- return
- let path ← lakeSetupSearchPath (←getLakePath) modules.toArray
- IO.println s!"Loading modules from: {path}"
- let doc ← load $ modules.map Name.mkSimple
- IO.println "Outputting HTML"
- htmlOutput doc
+def runDocGenCmd (p : Parsed) : IO UInt32 := do
+ -- let root := p.positionalArg! "root" |>.as! String
+ let modules : List String := p.variableArgsAs! String |>.toList
+ let res ← lakeSetup modules
+ match res with
+ | Except.ok (ws, leanHash) =>
+ IO.println s!"Loading modules from: {←searchPathRef.get}"
+ let doc ← load $ modules.map Name.mkSimple
+ IO.println "Outputting HTML"
+ htmlOutput doc ws leanHash
+ pure 0
+ | Except.error rc => pure rc
+
+def docGenCmd : Cmd := `[Cli|
+ "doc-gen4" VIA runDocGenCmd; ["0.0.1"]
+ "A documentation generator for Lean 4."
+
+ ARGS:
+ -- root : String; "The root URL to generate the HTML for (will be relative in the future)"
+ ...modules : String; "The modules to generate the HTML for"
+]
+
+def main (args : List String) : IO UInt32 :=
+ docGenCmd.validate args
diff --git a/lakefile.lean b/lakefile.lean
index cc8dd0e..d18d59c 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,6 +12,14 @@ package «doc-gen4» {
{
name := `Unicode
src := Source.git "https://github.com/xubaiw/Unicode.lean" "3b7b85472d42854a474099928a3423bb97d4fa64"
+ },
+ {
+ name := `Cli
+ src := Source.git "https://github.com/mhuisi/lean4-cli" "1f8663e3dafdcc11ff476d74ef9b99ae5bdaedd3"
+ },
+ {
+ name := `lake
+ src := Source.git "https://github.com/leanprover/lake" "9378575b5575f49a185d50130743a190a9be2f82"
}
]
}
diff --git a/lean-toolchain b/lean-toolchain
index 7c2b6c2..8e380ba 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-17
+leanprover/lean4:nightly-2022-03-06
diff --git a/static/declaration-data.js b/static/declaration-data.js
new file mode 100644
index 0000000..2b778d5
--- /dev/null
+++ b/static/declaration-data.js
@@ -0,0 +1,243 @@
+/**
+ * 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";
+
+const CACHE_DB_NAME = "declaration-data";
+const CACHE_DB_VERSION = 1;
+
+/**
+ * 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 = null;
+
+ /**
+ * 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 timestampUrl = new URL(
+ `${SITE_ROOT}declaration-data.timestamp`,
+ window.location
+ );
+ const dataUrl = new URL(
+ `${SITE_ROOT}declaration-data.bmp`,
+ window.location
+ );
+
+ const timestampRes = await fetch(timestampUrl);
+ const timestamp = await timestampRes.text();
+
+ // try to use cache first
+ const data = await fetchCachedDeclarationData(timestamp).catch(_e => null);
+ if (data) {
+ // if data is defined, use the cached one.
+ DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
+ } else {
+ // undefined. then fetch the data from the server.
+ const dataRes = await fetch(dataUrl);
+ const dataJson = await dataRes.json();
+ // the data is a map of name (original case) to declaration data.
+ const data = new Map(
+ dataJson.map(({ name, doc, link, docLink, sourceLink }) => [
+ name,
+ {
+ name,
+ lowerName: name.toLowerCase(),
+ lowerDoc: doc.toLowerCase(),
+ link,
+ docLink,
+ sourceLink,
+ },
+ ])
+ );
+ await cacheDeclarationData(timestamp, data);
+ DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
+ }
+ }
+ return DeclarationDataCenter.singleton;
+ }
+
+ /**
+ * Search for a declaration.
+ * @returns {Array}
+ */
+ search(pattern, strict = true) {
+ if (!pattern) {
+ return [];
+ }
+ if (strict) {
+ let decl = this.declarationData.get(pattern);
+ return decl ? [decl] : [];
+ } else {
+ return getMatches(this.declarationData, pattern);
+ }
+ }
+}
+
+function isSeparater(char) {
+ return char === "." || char === "_";
+}
+
+// HACK: the fuzzy matching is quite hacky
+
+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 {
+ name,
+ lowerName,
+ lowerDoc,
+ link,
+ docLink,
+ sourceLink,
+ } of declarations.values()) {
+ let err = matchCaseSensitive(name, lowerName, 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({
+ name,
+ err,
+ lowerName,
+ lowerDoc,
+ link,
+ docLink,
+ sourceLink,
+ });
+ }
+ }
+ return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults);
+}
+
+// TODO: refactor the indexedDB part to be more robust
+
+/**
+ * Get the indexedDB database, automatically initialized.
+ * @returns {Promise}
+ */
+async function getDeclarationDatabase() {
+ return new Promise((resolve, reject) => {
+ const request = indexedDB.open(CACHE_DB_NAME, CACHE_DB_VERSION);
+
+ request.onerror = function (event) {
+ reject(
+ new Error(
+ `fail to open indexedDB ${CACHE_DB_NAME} of version ${CACHE_DB_VERSION}`
+ )
+ );
+ };
+ request.onupgradeneeded = function (event) {
+ let db = event.target.result;
+ // We only need to store one object, so no key path or increment is needed.
+ db.createObjectStore("declaration");
+ };
+ request.onsuccess = function (event) {
+ resolve(event.target.result);
+ };
+ });
+}
+
+/**
+ * Store data in indexedDB object store.
+ * @param {string} timestamp
+ * @param {Map} data
+ */
+async function cacheDeclarationData(timestamp, data) {
+ let db = await getDeclarationDatabase();
+ let store = db
+ .transaction("declaration", "readwrite")
+ .objectStore("declaration");
+ return new Promise((resolve, reject) => {
+ let clearRequest = store.clear();
+ let addRequest = store.add(data, timestamp);
+
+ addRequest.onsuccess = function (event) {
+ resolve();
+ };
+ addRequest.onerror = function (event) {
+ reject(new Error(`fail to store declaration data`));
+ };
+ clearRequest.onerror = function (event) {
+ reject(new Error("fail to clear object store"));
+ };
+ });
+}
+
+/**
+ * Retrieve data from indexedDB database.
+ * @param {string} timestamp
+ * @returns {Promise|undefined>}
+ */
+async function fetchCachedDeclarationData(timestamp) {
+ let db = await getDeclarationDatabase();
+ let store = db
+ .transaction("declaration", "readonly")
+ .objectStore("declaration");
+ return new Promise((resolve, reject) => {
+ let transactionRequest = store.get(timestamp);
+ transactionRequest.onsuccess = function (event) {
+ resolve(event.result);
+ };
+ transactionRequest.onerror = function (event) {
+ reject(new Error(`fail to store declaration data`));
+ };
+ });
+}
diff --git a/static/find/find.js b/static/find/find.js
new file mode 100644
index 0000000..fbb9ca7
--- /dev/null
+++ b/static/find/find.js
@@ -0,0 +1,79 @@
+/**
+ * This module is used for the `/find` endpoint.
+ *
+ * Two basic kinds of search syntax are supported:
+ *
+ * 1. Query-Fragment syntax: `/find?pattern=Nat.add#doc` for documentation and `/find?pattern=Nat.add#src` for source code.
+ * 2. Fragment-Only syntax:`/find/#doc/Nat.add` for documentation and `/find/#src/Nat.add` for source code.
+ *
+ * Though both of them are valid, the first one is highly recommended, and the second one is for compatibility and taste.
+ *
+ * There are some extended usage for the QF syntax. For example, appending `strict=false` to the query part
+ * (`/find?pattern=Nat.add&strict=false#doc`) will allow you to use the fuzzy search, rather than strict match.
+ * Also, the fragment is extensible as well. For now only `#doc` and `#src` are implement, and the plain query without
+ * hash (`/find?pattern=Nat.add`) is used for computer-friendly data (semantic web is great! :P), while all other fragments
+ * fallback to the `#doc` view.
+ */
+
+import { SITE_ROOT } from "../site-root.js";
+import { DeclarationDataCenter } from "../declaration-data.js";
+
+/**
+ * We don't use browser's default hash and searchParams in case Lean declaration name
+ * can be like `«#»`, rather we manually handle the `window.location.href` with regex.
+ */
+const LEAN_FRIENDLY_URL_REGEX = /^[^?#]+(?:\?((?:[^«#»]|«.*»)*))?(?:#(.*))?$/;
+const LEAN_FRIENDLY_AND_SEPARATOR = /(? p.split(LEAN_FRIENDLY_EQUAL_SEPARATOR))
+ ?.filter((l) => l.length == 2 && l[0].length > 0)
+);
+const fragmentPaths = fragment?.split(LEAN_FRIENDLY_SLASH_SEPARATOR) ?? [];
+
+const pattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail then second, may be undefined
+const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true
+const view = fragmentPaths[0];
+
+findAndRedirect(pattern, strict, view);
+
+/**
+ * Find the result and redirect to the result page.
+ * @param {string} pattern the pattern to search for
+ * @param {string} view the view of the find result (`"doc"` or `"src"` for now)
+ */
+async function findAndRedirect(pattern, strict, view) {
+ // if no pattern provided, directly redirect to the 404 page
+ if (!pattern) {
+ window.location.replace(`${SITE_ROOT}404.html`);
+ }
+ // search for result
+ try {
+ const dataCenter = await DeclarationDataCenter.init();
+ let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array
+ // if no result found, redirect to the 404 page
+ if (!result) {
+ // TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found.
+ window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`);
+ } else {
+ // success, redirect to doc or source page, or to the semantic rdf.
+ if (!view) {
+ window.location.replace(result.link);
+ } else if (view == "doc") {
+ window.location.replace(result.docLink);
+ } else if (view == "src") {
+ window.location.replace(result.sourceLink);
+ } else {
+ // fallback to doc page
+ window.location.replace(result.docLink);
+ }
+ }
+ } catch (e) {
+ document.write(`Cannot fetch data, please check your network connection.\n${e}`);
+ }
+}
diff --git a/static/how-about.js b/static/how-about.js
new file mode 100644
index 0000000..5c03ffd
--- /dev/null
+++ b/static/how-about.js
@@ -0,0 +1,39 @@
+/**
+ * This module implements the `howabout` functionality in the 404 page.
+ */
+
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+const HOW_ABOUT = document.querySelector("#howabout");
+
+// Show url of the missing page
+if (HOW_ABOUT) {
+ 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("#", "");
+
+ // try to search for similar declarations
+ if (pattern) {
+ HOW_ABOUT.innerText = "Please wait a second. I'll try to help you.";
+ DeclarationDataCenter.init().then((dataCenter) => {
+ let results = dataCenter.search(pattern, false);
+ if (results.length > 0) {
+ HOW_ABOUT.innerText = "How about one of these instead:";
+ const ul = HOW_ABOUT.appendChild(document.createElement("ul"));
+ for (const { name, docLink } of results) {
+ const li = ul.appendChild(document.createElement("li"));
+ const a = li.appendChild(document.createElement("a"));
+ a.href = docLink;
+ a.appendChild(document.createElement("code")).innerText = name;
+ }
+ } 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 51adbd6..076dbf6 100644
--- a/static/mathjax-config.js
+++ b/static/mathjax-config.js
@@ -1,17 +1,41 @@
+/*
+ * 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: [['$$', '$$']]
- },
- 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'
- ],
- ignoreHtmlClass: 'tex2jax_ignore',
- processHtmlClass: 'tex2jax_process',
- },
-};
\ No newline at end of file
+ tex: {
+ 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",
+ ],
+ ignoreHtmlClass: "tex2jax_ignore",
+ processHtmlClass: "tex2jax_process",
+ },
+};
diff --git a/static/nav.js b/static/nav.js
index 7d5347d..ff8404e 100644
--- a/static/nav.js
+++ b/static/nav.js
@@ -1,248 +1,43 @@
-// 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 declURL = new URL(`${siteRoot}searchable_data.bmp`, window.location);
-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;
- }
-})()
-
-const declSearch = async (q) => getMatches(await getDecls(), q);
-
-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} of result) {
- const d = sr.appendChild(document.createElement('a'));
- d.innerText = decl;
- d.title = decl;
- d.href = `${siteRoot}find/${decl}`;
- }
- 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} of results) {
- const li = ul.appendChild(document.createElement('li'));
- const a = li.appendChild(document.createElement('a'));
- a.href = `${siteRoot}find/${decl}`;
- 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 836ef0e..5b075de 100644
--- a/static/search.js
+++ b/static/search.js
@@ -1,51 +1,118 @@
-function isSep(c) {
- return c === '.' || c === '_';
+/**
+ * This module is used to handle user's interaction with the search form.
+ */
+
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+const SEARCH_FORM = document.querySelector("#search_form");
+const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]");
+
+// Create an `div#search_results` to hold all search results.
+let sr = document.createElement("div");
+sr.id = "search_results";
+SEARCH_FORM.appendChild(sr);
+
+/**
+ * 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");
+ }
}
-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;
+/**
+ * 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);
+ }
+}
+
+/**
+ * Handle user input and perform search.
+ */
+function handleSearch(dataCenter, err, ev) {
+ const text = ev.target.value;
+
+ // If no input clear all.
+ if (!text) {
+ sr.removeAttribute("state");
+ removeAllChildren(sr);
+ return;
+ }
+
+ // searching
+ sr.setAttribute("state", "loading");
+
+ if (dataCenter) {
+ const result = dataCenter.search(text, false);
+
+ // in case user has updated the input.
+ if (ev.target.value != text) return;
+
+ // update search results
+ removeAllChildren(sr);
+ for (const { name, docLink } of result) {
+ const d = sr.appendChild(document.createElement("a"));
+ d.innerText = name;
+ d.title = name;
+ d.href = docLink;
}
+ }
+ // handle error
+ else {
+ removeAllChildren(sr);
+ const d = sr.appendChild(document.createElement("a"));
+ d.innerText = `Cannot fetch data, please check your network connection.\n${err}`;
+ }
+ sr.setAttribute("state", "done");
}
-function loadDecls(searchableDataCnt) {
- return searchableDataCnt.map(({name, description}) => [name, name.toLowerCase(), description.toLowerCase()])
-}
-
-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] of decls) {
- let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces);
-
- // 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});
- }
- }
- return results.sort(({err: a}, {err: b}) => a - b).slice(0, maxResults);
-}
-
-if (typeof process === 'object') { // NodeJS
- const data = loadDecls(JSON.parse(require('fs').readFileSync('searchable_data.bmp').toString()));
- console.log(getMatches(data, process.argv[2] || 'ltltle'));
-}
\ No newline at end of file
+DeclarationDataCenter.init()
+ .then((dataCenter) => {
+ // Search autocompletion.
+ SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev));
+ })
+ .catch(e => {
+ SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev));
+ });
diff --git a/static/site-root.js b/static/site-root.js
new file mode 100644
index 0000000..3dd39a3
--- /dev/null
+++ b/static/site-root.js
@@ -0,0 +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/style.css b/static/style.css
index a4e0c9a..d056b40 100644
--- a/static/style.css
+++ b/static/style.css
@@ -273,10 +273,15 @@ nav {
margin-top: 1ex;
}
-.nav details, .nav_link {
+.nav details > * {
padding-left: 2ex;
}
+.nav summary {
+ cursor: pointer;
+ padding-left: 0;
+}
+
.nav summary::marker {
font-size: 85%;
}
@@ -294,6 +299,10 @@ nav {
overflow-wrap: break-word;
}
+.nav_link {
+ overflow-wrap: break-word;
+}
+
.decl > div, .mod_doc {
padding-left: 8px;
padding-right: 8px;
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();
+ });
+}