feat: reduce JSON data size

DocGen4/Output/ToJson.lean

@@ -38,8 +38,13 @@ structure JsonModule where
 structure JsonHeaderIndex where
   headers : List (String × String) := []
 
+structure JsonIndexedDeclarationInfo where
+  kind : String
+  docLink : String
+  deriving FromJson, ToJson
+
 structure JsonIndex where
-  declarations : List (String × JsonDeclarationInfo) := []
+  declarations : List (String × JsonIndexedDeclarationInfo) := []
   instances : HashMap String (RBTree String Ord.compare) := .empty
   importedBy : HashMap String (Array String) := .empty
   modules : List (String × String) := []
@@ -71,7 +76,10 @@ def JsonHeaderIndex.addModule (index : JsonHeaderIndex) (module : JsonModule) :
 def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM JsonIndex := do
   let mut index := index
   let newModule := (module.name, ← moduleNameToLink (String.toName module.name))
-  let newDecls := module.declarations.map (fun d => (d.info.name, d.info))
+  let newDecls := module.declarations.map (fun d => (d.info.name, {
+    kind := d.info.kind,
+    docLink := d.info.docLink,
+  }))
   index := { index with
     modules := newModule :: index.modules
     declarations := newDecls ++ index.declarations

static/declaration-data.js

@@ -168,12 +168,9 @@ function getMatches(declarations, pattern, allowedKinds = undefined, maxResults
   const lowerPats = pattern.toLowerCase().split(/\s/g);
   const patNoSpaces = pattern.replace(/\s/g, "");
   const results = [];
-  for (const [_, {
+  for (const [name, {
-    name,
     kind,
-    doc,
     docLink,
-    sourceLink,
   }] of Object.entries(declarations)) {
     // Apply "kind" filter
     if (allowedKinds !== undefined) {
@@ -182,26 +179,14 @@ function getMatches(declarations, pattern, allowedKinds = undefined, maxResults
       }
     }
     const lowerName = name.toLowerCase();
-    const lowerDoc = doc.toLowerCase();
     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,
         kind,
-        doc,
         err,
         lowerName,
-        lowerDoc,
         docLink,
-        sourceLink,
       });
     }
   }

static/find/find.js

@@ -80,8 +80,6 @@ async function findAndRedirect(pattern, strict, 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);

static/importedBy.js

@@ -3,7 +3,7 @@ import { DeclarationDataCenter } from "./declaration-data.js";
 fillImportedBy();
 
 async function fillImportedBy() {
-  if (!MODULE_NAME) {
+  if (typeof(MODULE_NAME) == "undefined") {
     return;
   }
   const dataCenter = await DeclarationDataCenter.init();

static/search.js

@@ -112,7 +112,7 @@ function handleSearch(dataCenter, err, ev, sr, maxResults, autocomplete) {
   
     // update autocomplete results
     removeAllChildren(sr);
-    for (const { name, kind, doc, docLink } of result) {
+    for (const { name, kind, docLink } of result) {
       const row = sr.appendChild(document.createElement("div"));
       row.classList.add("search_result")
       const linkdiv = row.appendChild(document.createElement("div"))
@@ -121,11 +121,6 @@ function handleSearch(dataCenter, err, ev, sr, maxResults, autocomplete) {
       link.innerText = name;
       link.title = name;
       link.href = SITE_ROOT + docLink;
-      if (!autocomplete) {
-        const doctext = row.appendChild(document.createElement("div"));
-        doctext.innerText = doc
-        doctext.classList.add("result_doc")
-      }
     }
   }
   // handle error