diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 82d3a26..ae4d03a 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -74,10 +74,10 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do for (_, mod) in result.moduleInfo.toArray do for decl in filterMapDocInfo mod.members do let name := decl.getName.toString - let description := decl.getDocString.getD "" + let doc := decl.getDocString.getD "" let link := Id.run <| ReaderT.run (declNameToLink decl.getName) config let source := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config - let obj := Json.mkObj [("name", name), ("description", description), ("link", link), ("source", source)] + let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("source", source)] declList := declList.push obj let json := Json.arr declList diff --git a/static/declaration-data.js b/static/declaration-data.js index ec72aa8..0d07024 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -1,6 +1,6 @@ /** * This module is a wrapper that facilitates manipulating the declaration data. - * + * * Please see {@link DeclarationDataCenter} for more information. */ @@ -8,16 +8,16 @@ 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. - * + * The declaration data. Users should not interact directly with this field. + * * *NOTE:* This is not made private to support legacy browsers. */ - declarationData = []; + declarationData = null; /** * Used to implement the singleton, in case we need to fetch data mutiple times in the same page. @@ -26,7 +26,7 @@ export class DeclarationDataCenter { /** * Construct a DeclarationDataCenter with given data. - * + * * Please use {@link DeclarationDataCenter.init} instead, which automates the data fetching process. * @param {*} declarationData */ @@ -46,13 +46,19 @@ export class DeclarationDataCenter { ); 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, - ]); + // the data is a map of name (original case) to declaration data. + const data = new Map( + json.map(({ name, doc, link, source: sourceLink }) => [ + name, + { + name, + lowerName: name.toLowerCase(), + lowerDoc: doc.toLowerCase(), + link, + sourceLink, + }, + ]) + ); DeclarationDataCenter.singleton = new DeclarationDataCenter(data); } return DeclarationDataCenter.singleton; @@ -66,8 +72,12 @@ export class DeclarationDataCenter { if (!pattern) { return []; } - // TODO: implement strict - return getMatches(this.declarationData, pattern); + if (strict) { + let decl = this.declarationData.get(pattern); + return decl ? [decl] : []; + } else { + return getMatches(this.declarationData, pattern); + } } } @@ -75,20 +85,15 @@ function isSeparater(char) { return char === "." || char === "_"; } -function matchCaseSensitive( - declName, - lowerDeclName, - pattern -) { +// 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] - ) { + 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; @@ -109,18 +114,24 @@ 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); + for (const { + name, + lowerName, + lowerDoc, + link, + sourceLink, + } of declarations.values()) { + let err = matchCaseSensitive(name, lowerName, patNoSpaces); // match all words as substrings of docstring if ( - !(err < 3) && + err >= 3 && pattern.length > 3 && lowerPats.every((l) => lowerDoc.indexOf(l) != -1) ) { err = 3; } if (err !== undefined) { - results.push({ decl, err, link, source }); + results.push({ name, err, lowerName, lowerDoc, link, sourceLink }); } } 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 7fcb9ec..75b5507 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -7,21 +7,19 @@ 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 results = dataCenter.search(pattern, true); + if (results.length == 0) { + // if there is no exact match, redirect to 404 page to use fuzzy match + window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`); + } else { + // redirect to doc or source page. + window.location.replace(isSource ? results[0].sourceLink : results[0].link); } } -let hash = window.location.hash.split("#"); +let hash = window.location.hash.replace("#", ""); -if (hash.length == 0) { - window.location.replace(`${SITE_ROOT}/404.html`); -} - -if (hash[1].endsWith("/src")) { +if (hash.endsWith("/src")) { findRedirect(hash.replace("/src", ""), true); } else { findRedirect(hash, false); diff --git a/static/how-about.js b/static/how-about.js index 421f6e4..cb9832b 100644 --- a/static/how-about.js +++ b/static/how-about.js @@ -6,9 +6,8 @@ import { DeclarationDataCenter } from "./declaration-data.js"; const HOW_ABOUT = document.querySelector("#howabout"); +// Show url of the missing page 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 = @@ -17,19 +16,24 @@ if (HOW_ABOUT) { // 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; + // 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); + if (results.length > 0) { + HOW_ABOUT.innerText = "How about one of these instead:"; + const ul = HOW_ABOUT.appendChild(document.createElement("ul")); + for (const { name, 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 = 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"; } - } 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"; - } - }); + }); + } }