From 59707cda58d4cf5863daae5840a753f535fc034d Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Mon, 21 Feb 2022 01:12:49 +0800 Subject: [PATCH] refactor: use js for find --- DocGen4/Output.lean | 16 +++++++++++----- DocGen4/Output/Base.lean | 1 + DocGen4/Output/Find.lean | 16 +++++++++++----- DocGen4/Output/Template.lean | 6 ++---- static/find/find.js | 14 ++++++++++++++ static/nav.js | 29 +++++------------------------ static/search.js | 29 +++++++++++++++++++++++++---- 7 files changed, 69 insertions(+), 42 deletions(-) create mode 100644 static/find/find.js diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 9b7407d..85c60cf 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -65,6 +65,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker} let basePath := FilePath.mk "." / "build" / "doc" let indexHtml := ReaderT.run index config + let findHtml := ReaderT.run find config let notFoundHtml := ReaderT.run notFound config FS.createDirAll basePath FS.createDirAll (basePath / "find") @@ -72,12 +73,12 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let mut declList := #[] for (_, mod) in result.moduleInfo.toArray do for decl in filterMapDocInfo mod.members do - let findHtml := ReaderT.run (findRedirectHtml decl.getName) config - let findDir := basePath / "find" / decl.getName.toString - FS.createDirAll findDir - FS.writeFile (findDir / "index.html") findHtml.toString - let obj := Json.mkObj [("name", decl.getName.toString), ("description", decl.getDocString.getD "")] + let name := decl.getName.toString + let description := decl.getDocString.getD "" + let link := Id.run <| ReaderT.run (declNameToLink decl.getName) config + let obj := Json.mkObj [("name", name), ("description", description), ("link", link)] declList := declList.push obj + let json := Json.arr declList FS.writeFile (basePath / "searchable_data.bmp") json.compress @@ -88,6 +89,11 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do FS.writeFile (basePath / "search.js") searchJs FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs FS.writeFile (basePath / "site-root.js") s!"export const SITE_ROOT = \"{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 let path := moduleNameToFile basePath module diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 4579f69..6020686 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -49,6 +49,7 @@ section Static def styleCss : String := include_str "./static/style.css" def navJs : String := include_str "./static/nav.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" end Static diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean index 41b82dd..60e56ac 100644 --- a/DocGen4/Output/Find.lean +++ b/DocGen4/Output/Find.lean @@ -6,10 +6,16 @@ namespace Output open scoped DocGen4.Jsx open Lean -def findRedirectHtml (decl : Name) : HtmlM Html := do - let res ← getResult - let url ← declNameToLink decl - let contentString := s!"0;url={url}" - pure $ Html.element "meta" false #[("http-equiv", "refresh"), ("content", contentString)] #[] +def find : HtmlM Html := do + pure + + + + + + + + end Output end DocGen4 + diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 51868ec..d4f358f 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -26,13 +26,11 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do - - - - + + diff --git a/static/find/find.js b/static/find/find.js new file mode 100644 index 0000000..70eb818 --- /dev/null +++ b/static/find/find.js @@ -0,0 +1,14 @@ +import { SITE_ROOT } from "../site-root.js"; +import { declSearch } from "../search.js"; + +let splits = window.location.href.split("#"); + +if (splits.length < 2) { + window.location.replace(`${SITE_ROOT}/404.html`); +} + +declSearch(splits[1]).then((results) => { + window.location.replace(results[0].link); +}).catch(() => { + window.location.replace(`${SITE_ROOT}404.html`); +}); \ No newline at end of file diff --git a/static/nav.js b/static/nav.js index 18ff91b..3889da3 100644 --- a/static/nav.js +++ b/static/nav.js @@ -1,5 +1,4 @@ -import { SITE_ROOT } from "./site-root.js"; -import { loadDecls, getMatches } from "./search.js"; +import { declSearch } from "./search.js"; // Persistent expansion cookie for the file tree // --------------------------------------------- @@ -109,24 +108,6 @@ if (tse != null) { // Simple declaration search // ------------------------- -const declURL = new URL(`${SITE_ROOT}searchable_data.bmp`, window.location); -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; - } -})() - -const declSearch = async (q) => getMatches(await getDecls(), q); - const srId = 'search_results'; document.getElementById('search_form') .appendChild(document.createElement('div')) @@ -191,11 +172,11 @@ searchInput.addEventListener('input', async (ev) => { const oldSR = document.getElementById('search_results'); const sr = oldSR.cloneNode(false); - for (const {decl} of result) { + for (const {decl, link} of result) { const d = sr.appendChild(document.createElement('a')); d.innerText = decl; d.title = decl; - d.href = `${SITE_ROOT}find/${decl}`; + d.href = link; } sr.setAttribute('state', 'done'); oldSR.replaceWith(sr); @@ -222,10 +203,10 @@ if (howabout) { declSearch(query).then((results) => { howabout.innerText = 'How about one of these instead:'; const ul = howabout.appendChild(document.createElement('ul')); - for (const {decl} of results) { + for (const {decl, link} of results) { const li = ul.appendChild(document.createElement('li')); const a = li.appendChild(document.createElement('a')); - a.href = `${SITE_ROOT}find/${decl}`; + a.href = link; a.appendChild(document.createElement('code')).innerText = decl; } }); diff --git a/static/search.js b/static/search.js index 5e5f220..abdc579 100644 --- a/static/search.js +++ b/static/search.js @@ -1,3 +1,5 @@ +import { SITE_ROOT } from "./site-root.js"; + function isSep(c) { return c === '.' || c === '_'; } @@ -23,14 +25,14 @@ function matchCaseSensitive(declName, lowerDeclName, pat) { } export function loadDecls(searchableDataCnt) { - return searchableDataCnt.map(({name, description}) => [name, name.toLowerCase(), description.toLowerCase()]) + return searchableDataCnt.map(({name, description, link}) => [name, name.toLowerCase(), description.toLowerCase(), link]); } 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] of decls) { + for (const [decl, lowerDecl, lowerDoc, link] of decls) { let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces); // match all words as substrings of docstring @@ -39,8 +41,27 @@ export function getMatches(decls, pat, maxResults = 30) { } if (err !== undefined) { - results.push({decl, err}); + results.push({decl, err, link}); } } return results.sort(({err: a}, {err: b}) => a - b).slice(0, maxResults); -} \ No newline at end of file +} + +const declURL = new URL(`${SITE_ROOT}searchable_data.bmp`, window.location); + +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; + } +})() + +export const declSearch = async (q) => getMatches(await getDecls(), q); \ No newline at end of file