diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean index 3fc7ff2..4d87394 100644 --- a/DocGen4/Output/ToJson.lean +++ b/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 diff --git a/static/declaration-data.js b/static/declaration-data.js index 5dbb5fe..c5bcdcd 100644 --- a/static/declaration-data.js +++ b/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 [_, { - name, + for (const [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, }); } } diff --git a/static/find/find.js b/static/find/find.js index 038a1a1..e35312a 100644 --- a/static/find/find.js +++ b/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); diff --git a/static/importedBy.js b/static/importedBy.js index dab932d..5eb7fca 100644 --- a/static/importedBy.js +++ b/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(); diff --git a/static/search.js b/static/search.js index 809f4bd..38c7e18 100644 --- a/static/search.js +++ b/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