refactor: clean up javascript code
Xubai Wang
parent
9e867f5151
commit
f23556739f
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ def find : HtmlM Html := do
|
|||
pure
|
||||
<html lang="en">
|
||||
<head>
|
||||
<link rel="preload" href={s!"{←getRoot}searchable_data.bmp"}/>
|
||||
<link rel="preload" href={s!"{←getRoot}declaration-data.bmp"}/>
|
||||
<script type="module" async="true" src={s!"./find.js"}></script>
|
||||
</head>
|
||||
<body></body>
|
||||
|
|
|
|||
|
|
@ -24,13 +24,15 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
|
|||
<link rel="stylesheet" href={s!"{←getRoot}style.css"}/>
|
||||
<link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>
|
||||
<link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
|
||||
<link rel="prefetch" href={s!"{←getRoot}searchable_data.bmp"}/>
|
||||
<link rel="prefetch" href={s!"{←getRoot}declaration-data.bmp"}/>
|
||||
|
||||
<script defer="true" src={s!"{←getRoot}mathjax-config.js"}></script>
|
||||
<script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
|
||||
<script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
|
||||
|
||||
<script type="module" src={s!"{←getRoot}nav.js"}></script>
|
||||
<script type="module" src={s!"{←getRoot}search.js"}></script>
|
||||
<script type="module" src={s!"{←getRoot}how-about.js"}></script>
|
||||
|
||||
</head>
|
||||
|
||||
|
|
|
|||
|
|
@ -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<DeclarationDataCenter>}
|
||||
*/
|
||||
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<any>}
|
||||
*/
|
||||
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);
|
||||
}
|
||||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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";
|
||||
}
|
||||
});
|
||||
}
|
||||
|
|
@ -1,26 +1,41 @@
|
|||
/*
|
||||
* This file is for configing MathJax behavior.
|
||||
* Seehttps://docs.mathjax.org/en/latest/web/configuration.html
|
||||
*/
|
||||
|
||||
/**
|
||||
* 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",
|
||||
},
|
||||
};
|
||||
237
static/nav.js
237
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" });
|
||||
}
|
||||
143
static/search.js
143
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;
|
||||
|
||||
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");
|
||||
}
|
||||
}
|
||||
|
||||
export function loadDecls(searchableDataCnt) {
|
||||
return searchableDataCnt.map(({name, description, link, source}) => [name, name.toLowerCase(), description.toLowerCase(), link, source]);
|
||||
/**
|
||||
* Perform search (when enter is pressed).
|
||||
*/
|
||||
function handleSearchEnter() {
|
||||
const sel =
|
||||
sr.querySelector(`.selected`) ||
|
||||
sr.firstChild;
|
||||
sel.click();
|
||||
}
|
||||
|
||||
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);
|
||||
/**
|
||||
* 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;
|
||||
}
|
||||
});
|
||||
|
||||
// match all words as substrings of docstring
|
||||
if (!(err < 3) && pat.length > 3 && lowerPats.every(l => lowerDoc.indexOf(l) != -1)) {
|
||||
err = 3;
|
||||
/**
|
||||
* Remove all children of a DOM node.
|
||||
*/
|
||||
function removeAllChildren(node) {
|
||||
while (node.firstChild) {
|
||||
node.removeChild(node.lastChild);
|
||||
}
|
||||
|
||||
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);
|
||||
/**
|
||||
* Search autocompletion.
|
||||
*/
|
||||
SEARCH_INPUT.addEventListener("input", async (ev) => {
|
||||
const text = ev.target.value;
|
||||
|
||||
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;
|
||||
// If no input clear all.
|
||||
if (!text) {
|
||||
sr.removeAttribute("state");
|
||||
removeAllChildren(sr);
|
||||
return;
|
||||
}
|
||||
})()
|
||||
|
||||
export const declSearch = async (q) => getMatches(await getDecls(), q);
|
||||
// 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");
|
||||
});
|
||||
|
|
|
|||
|
|
@ -1 +1,4 @@
|
|||
/**
|
||||
* Get the site root, {siteRoot} is to be replaced by doc-gen4.
|
||||
*/
|
||||
export const SITE_ROOT = "{siteRoot}";
|
||||
|
|
@ -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();
|
||||
});
|
||||
}
|
||||
Loading…
Reference in New Issue