refactor: use strict match for find

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

static/declaration-data.js

@@ -17,7 +17,7 @@ export class DeclarationDataCenter {
    *
    * *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.
@@ -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 }) => [
+      // 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.toLowerCase(),
+          {
-        description.toLowerCase(),
+            name,
+            lowerName: name.toLowerCase(),
+            lowerDoc: doc.toLowerCase(),
             link,
-        source,
+            sourceLink,
-      ]);
+          },
+        ])
+      );
       DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
     }
     return DeclarationDataCenter.singleton;
@@ -66,29 +72,28 @@ export class DeclarationDataCenter {
     if (!pattern) {
       return [];
     }
-    // TODO: implement strict
+    if (strict) {
+      let decl = this.declarationData.get(pattern);
+      return decl ? [decl] : [];
+    } else {
       return getMatches(this.declarationData, pattern);
     }
   }
+}
 
 function isSeparater(char) {
   return char === "." || char === "_";
 }
 
-function matchCaseSensitive(
+// HACK: the fuzzy matching is quite hacky
-  declName,
+
-  lowerDeclName,
+function matchCaseSensitive(declName, lowerDeclName, pattern) {
-  pattern
-) {
   let i = 0,
     j = 0,
     err = 0,
     lastMatch = 0;
   while (i < declName.length && j < pattern.length) {
-    if (
+    if (pattern[j] === declName[i] || pattern[j] === lowerDeclName[i]) {
-      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) {
+  for (const {
-    let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces);
+    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);

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, true);
-    let results = dataCenter.search(pattern);
+  if (results.length == 0) {
-    window.location.replace(isSource ? results[0].source : results[0].link);
+    // if there is no exact match, redirect to 404 page to use fuzzy match
-  } catch {
+    window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`);
-    window.location.replace(`${SITE_ROOT}404.html`);
+  } 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) {
+if (hash.endsWith("/src")) {
-  window.location.replace(`${SITE_ROOT}/404.html`);
-}
-
-if (hash[1].endsWith("/src")) {
   findRedirect(hash.replace("/src", ""), true);
 } else {
   findRedirect(hash, false);

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("#", "");
 
+  // 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 { decl, link } of results) {
+        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 = decl;
+          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";
+        HOW_ABOUT.innerText =
+          "Sorry, I cannot find any similar declarations. Check the link or use the module navigation to find what you want :P";
       }
     });
   }
+}