From 9f13773a7db836088c4142d3d39ae382d6c225d3 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 22:54:57 +0800 Subject: [PATCH 01/23] refactor: use json ext instead of bmp --- DocGen4/Output.lean | 2 +- static/nav.js | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 4f549c2..8d2b30e 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -80,7 +80,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do declList := declList.push obj let json := Json.arr declList - FS.writeFile (basePath / "searchable_data.bmp") json.compress + FS.writeFile (basePath / "searchable_data.json") json.compress FS.writeFile (basePath / "index.html") indexHtml.toString FS.writeFile (basePath / "style.css") styleCss FS.writeFile (basePath / "404.html") notFoundHtml.toString diff --git a/static/nav.js b/static/nav.js index 7d5347d..b741863 100644 --- a/static/nav.js +++ b/static/nav.js @@ -106,7 +106,7 @@ if (tse != null) { // Simple declaration search // ------------------------- -const declURL = new URL(`${siteRoot}searchable_data.bmp`, window.location); +const declURL = new URL(`${siteRoot}searchable_data.json`, window.location); const getDecls = (() => { let decls; return () => { From b9c5109aaf3bde51c27ad0fbdcde7dc084159ee7 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 23:05:35 +0800 Subject: [PATCH 02/23] pref: prefetch search data --- DocGen4/Output/Template.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 8ed58ee..232df38 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -18,6 +18,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do + {title} From a89cf7d7a4c26a83ff5f0da9758f97c3c237819e Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 23:24:08 +0800 Subject: [PATCH 03/23] refactor: move siteRoot to separate file --- DocGen4/Output.lean | 3 ++- DocGen4/Output/Template.lean | 6 ++---- static/mathjax-config.js | 39 ++++++++++++++++++++++-------------- static/nav.js | 2 +- 4 files changed, 29 insertions(+), 21 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 8d2b30e..2509c25 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -80,13 +80,14 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do declList := declList.push obj let json := Json.arr declList - FS.writeFile (basePath / "searchable_data.json") json.compress + FS.writeFile (basePath / "searchable-data.json") json.compress FS.writeFile (basePath / "index.html") indexHtml.toString FS.writeFile (basePath / "style.css") styleCss FS.writeFile (basePath / "404.html") notFoundHtml.toString FS.writeFile (basePath / "nav.js") navJs FS.writeFile (basePath / "search.js") searchJs FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs + FS.writeFile (basePath / "site-root.js") s!"siteRoot = \"{config.root}\""; 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/Template.lean b/DocGen4/Output/Template.lean index 232df38..9181b47 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -18,7 +18,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do - + {title} @@ -44,9 +44,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do {←navbar} -- Lean in JS in HTML in Lean...very meta - + -- TODO Add more js stuff diff --git a/static/mathjax-config.js b/static/mathjax-config.js index 51adbd6..9e470bc 100644 --- a/static/mathjax-config.js +++ b/static/mathjax-config.js @@ -1,17 +1,26 @@ +/* + * This file is for configing MathJax behavior. + * Seehttps://docs.mathjax.org/en/latest/web/configuration.html + */ + +/** + * This configuration is copied from old doc-gen3 + * https://github.com/leanprover-community/doc-gen + */ MathJax = { - tex: { - inlineMath: [['$', '$']], - displayMath: [['$$', '$$']] - }, - options: { - skipHtmlTags: [ - 'script', 'noscript', 'style', 'textarea', 'pre', - 'code', 'annotation', 'annotation-xml', - 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name', - 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields', - 'constructor', 'constructors', 'instances' - ], - ignoreHtmlClass: 'tex2jax_ignore', - processHtmlClass: 'tex2jax_process', - }, + tex: { + inlineMath: [['$', '$']], + displayMath: [['$$', '$$']] + }, + options: { + skipHtmlTags: [ + 'script', 'noscript', 'style', 'textarea', 'pre', + 'code', 'annotation', 'annotation-xml', + 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name', + 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields', + 'constructor', 'constructors', 'instances' + ], + ignoreHtmlClass: 'tex2jax_ignore', + processHtmlClass: 'tex2jax_process', + }, }; \ No newline at end of file diff --git a/static/nav.js b/static/nav.js index b741863..75b82fd 100644 --- a/static/nav.js +++ b/static/nav.js @@ -106,7 +106,7 @@ if (tse != null) { // Simple declaration search // ------------------------- -const declURL = new URL(`${siteRoot}searchable_data.json`, window.location); +const declURL = new URL(`${siteRoot}searchable-data.json`, window.location); const getDecls = (() => { let decls; return () => { From 73f790635728581245cff2180e0de75aa0364b94 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 23:42:46 +0800 Subject: [PATCH 04/23] refactor: move script into head --- DocGen4/Output/Template.lean | 56 +++++++++++++++++++----------------- 1 file changed, 29 insertions(+), 27 deletions(-) diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 9181b47..258bdde 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -15,45 +15,47 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do pure + + {title} + + + + - {title} - - + + + + + + + + - + -
-

Documentation

-

{title}

- -- TODO: Replace this form with our own search -
- - - -
-
+
+

Documentation

+

{title}

+ -- TODO: Replace this form with our own search +
+ + + +
+
- [site] - - {←navbar} + [site] + + {←navbar} - -- Lean in JS in HTML in Lean...very meta - - - -- TODO Add more js stuff - - - -- mathjax - - - + From 842e24324104f99c19d65f9ef2a9b803a3341295 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 23:45:31 +0800 Subject: [PATCH 05/23] revert: use bmp extension again --- DocGen4/Output.lean | 2 +- DocGen4/Output/Template.lean | 2 +- static/nav.js | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 2509c25..2016559 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -80,7 +80,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do declList := declList.push obj let json := Json.arr declList - FS.writeFile (basePath / "searchable-data.json") json.compress + FS.writeFile (basePath / "searchable_data.bmp") json.compress FS.writeFile (basePath / "index.html") indexHtml.toString FS.writeFile (basePath / "style.css") styleCss FS.writeFile (basePath / "404.html") notFoundHtml.toString diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 258bdde..fa15cd1 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -24,7 +24,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do - + diff --git a/static/nav.js b/static/nav.js index 75b82fd..7d5347d 100644 --- a/static/nav.js +++ b/static/nav.js @@ -106,7 +106,7 @@ if (tse != null) { // Simple declaration search // ------------------------- -const declURL = new URL(`${siteRoot}searchable-data.json`, window.location); +const declURL = new URL(`${siteRoot}searchable_data.bmp`, window.location); const getDecls = (() => { let decls; return () => { From 5e93038023233b237057d325b1bca754ac6fa46a Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Mon, 21 Feb 2022 00:06:15 +0800 Subject: [PATCH 06/23] refactor: use js modules --- DocGen4/Output.lean | 2 +- DocGen4/Output/Template.lean | 7 ++++--- static/nav.js | 9 ++++++--- static/search.js | 9 ++------- 4 files changed, 13 insertions(+), 14 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 2016559..9b7407d 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -87,7 +87,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do FS.writeFile (basePath / "nav.js") navJs FS.writeFile (basePath / "search.js") searchJs FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs - FS.writeFile (basePath / "site-root.js") s!"siteRoot = \"{config.root}\""; + FS.writeFile (basePath / "site-root.js") s!"export const SITE_ROOT = \"{config.root}\";"; 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/Template.lean b/DocGen4/Output/Template.lean index fa15cd1..51868ec 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -26,9 +26,10 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do - - - + + + + diff --git a/static/nav.js b/static/nav.js index 7d5347d..18ff91b 100644 --- a/static/nav.js +++ b/static/nav.js @@ -1,3 +1,6 @@ +import { SITE_ROOT } from "./site-root.js"; +import { loadDecls, getMatches } from "./search.js"; + // Persistent expansion cookie for the file tree // --------------------------------------------- @@ -106,7 +109,7 @@ if (tse != null) { // Simple declaration search // ------------------------- -const declURL = new URL(`${siteRoot}searchable_data.bmp`, window.location); +const declURL = new URL(`${SITE_ROOT}searchable_data.bmp`, window.location); const getDecls = (() => { let decls; return () => { @@ -192,7 +195,7 @@ searchInput.addEventListener('input', async (ev) => { const d = sr.appendChild(document.createElement('a')); d.innerText = decl; d.title = decl; - d.href = `${siteRoot}find/${decl}`; + d.href = `${SITE_ROOT}find/${decl}`; } sr.setAttribute('state', 'done'); oldSR.replaceWith(sr); @@ -222,7 +225,7 @@ if (howabout) { for (const {decl} of results) { const li = ul.appendChild(document.createElement('li')); const a = li.appendChild(document.createElement('a')); - a.href = `${siteRoot}find/${decl}`; + a.href = `${SITE_ROOT}find/${decl}`; a.appendChild(document.createElement('code')).innerText = decl; } }); diff --git a/static/search.js b/static/search.js index 836ef0e..5e5f220 100644 --- a/static/search.js +++ b/static/search.js @@ -22,11 +22,11 @@ function matchCaseSensitive(declName, lowerDeclName, pat) { } } -function loadDecls(searchableDataCnt) { +export function loadDecls(searchableDataCnt) { return searchableDataCnt.map(({name, description}) => [name, name.toLowerCase(), description.toLowerCase()]) } -function getMatches(decls, pat, maxResults = 30) { +export function getMatches(decls, pat, maxResults = 30) { const lowerPats = pat.toLowerCase().split(/\s/g); const patNoSpaces = pat.replace(/\s/g, ''); const results = []; @@ -43,9 +43,4 @@ function getMatches(decls, pat, maxResults = 30) { } } return results.sort(({err: a}, {err: b}) => a - b).slice(0, maxResults); -} - -if (typeof process === 'object') { // NodeJS - const data = loadDecls(JSON.parse(require('fs').readFileSync('searchable_data.bmp').toString())); - console.log(getMatches(data, process.argv[2] || 'ltltle')); } \ No newline at end of file From 59707cda58d4cf5863daae5840a753f535fc034d Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Mon, 21 Feb 2022 01:12:49 +0800 Subject: [PATCH 07/23] 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 From bc0dd3b48a80dfe3cf116e68d0fe8398d26f740e Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Mon, 21 Feb 2022 01:38:12 +0800 Subject: [PATCH 08/23] feat: add src endpoint --- DocGen4/Output.lean | 3 ++- static/find/find.js | 18 +++++++++++++----- static/search.js | 6 +++--- 3 files changed, 18 insertions(+), 9 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 85c60cf..0860072 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -76,7 +76,8 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do 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)] + let source := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config + let obj := Json.mkObj [("name", name), ("description", description), ("link", link), ("source", source)] declList := declList.push obj let json := Json.arr declList diff --git a/static/find/find.js b/static/find/find.js index 70eb818..480f725 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -1,14 +1,22 @@ import { SITE_ROOT } from "../site-root.js"; import { declSearch } from "../search.js"; +async function findRedirect(query, isSource) { + return declSearch(query).then((results) => { + window.location.replace(isSource? results[0].source : results[0].link); + }).catch(() => { + window.location.replace(`${SITE_ROOT}404.html`); + }); +} + 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 +if (splits[1].endsWith("/src")) { + findRedirect(splits[1].replace("/src", ""), true); +} else { + findRedirect(splits[1], false); +} diff --git a/static/search.js b/static/search.js index abdc579..3449036 100644 --- a/static/search.js +++ b/static/search.js @@ -25,14 +25,14 @@ function matchCaseSensitive(declName, lowerDeclName, pat) { } export function loadDecls(searchableDataCnt) { - return searchableDataCnt.map(({name, description, link}) => [name, name.toLowerCase(), description.toLowerCase(), link]); + return searchableDataCnt.map(({name, description, link, source}) => [name, name.toLowerCase(), description.toLowerCase(), link, source]); } 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, link] of decls) { + for (const [decl, lowerDecl, lowerDoc, link, source] of decls) { let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces); // match all words as substrings of docstring @@ -41,7 +41,7 @@ export function getMatches(decls, pat, maxResults = 30) { } if (err !== undefined) { - results.push({decl, err, link}); + results.push({decl, err, link, source}); } } return results.sort(({err: a}, {err: b}) => a - b).slice(0, maxResults); From 9e867f5151928c5f16a243d2fb65d968fc0d542f Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Mon, 21 Feb 2022 23:29:23 +0800 Subject: [PATCH 09/23] refactor: make site-root an actual file --- DocGen4/Output.lean | 2 +- DocGen4/Output/Base.lean | 1 + static/site-root.js | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) create mode 100644 static/site-root.js diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 0860072..dcf51d0 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -89,7 +89,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do FS.writeFile (basePath / "nav.js") navJs 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 / "site-root.js") (siteRootJs.replace "{siteRoot}" config.root) FS.writeFile (basePath / "find" / "index.html") findHtml.toString FS.writeFile (basePath / "find" / "find.js") findJs diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 6020686..0188511 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -47,6 +47,7 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := section Static def styleCss : String := include_str "./static/style.css" + def siteRootJs : String := include_str "./static/site-root.js" 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" diff --git a/static/site-root.js b/static/site-root.js new file mode 100644 index 0000000..0663d6b --- /dev/null +++ b/static/site-root.js @@ -0,0 +1 @@ +export const SITE_ROOT = "{siteRoot}"; \ No newline at end of file From f23556739f070a1aa5578e1464cc26f8868a3d78 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Tue, 22 Feb 2022 12:40:14 +0800 Subject: [PATCH 10/23] refactor: clean up javascript code --- DocGen4/Output.lean | 19 ++- DocGen4/Output/Base.lean | 2 + DocGen4/Output/Find.lean | 2 +- DocGen4/Output/Template.lean | 4 +- static/declaration-data.js | 127 +++++++++++++++++++ static/find/find.js | 30 +++-- static/how-about.js | 35 +++++ static/mathjax-config.js | 45 ++++--- static/nav.js | 239 ++++------------------------------- static/search.js | 157 ++++++++++++++--------- static/site-root.js | 3 + static/tactic.js | 61 +++++++++ 12 files changed, 414 insertions(+), 310 deletions(-) create mode 100644 static/declaration-data.js create mode 100644 static/how-about.js create mode 100644 static/tactic.js diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index dcf51d0..82d3a26 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -82,18 +82,23 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let json := Json.arr declList - FS.writeFile (basePath / "searchable_data.bmp") json.compress FS.writeFile (basePath / "index.html") indexHtml.toString - FS.writeFile (basePath / "style.css") styleCss FS.writeFile (basePath / "404.html") notFoundHtml.toString + FS.writeFile (basePath / "find" / "index.html") findHtml.toString + + FS.writeFile (basePath / "style.css") styleCss + + let declarationDataPath := basePath / "declaration-data.bmp" + FS.writeFile declarationDataPath json.compress + FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec + + FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" config.root) + FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs FS.writeFile (basePath / "nav.js") navJs + FS.writeFile (basePath / "find" / "find.js") findJs + FS.writeFile (basePath / "how-about.js") howAboutJs FS.writeFile (basePath / "search.js") searchJs FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs - FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" 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 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 0188511..20443f8 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -48,7 +48,9 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := section Static def styleCss : String := include_str "./static/style.css" def siteRootJs : String := include_str "./static/site-root.js" + def declarationDataCenterJs : String := include_str "./static/declaration-data.js" def navJs : String := include_str "./static/nav.js" + def howAboutJs : String := include_str "./static/how-about.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" diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean index 60e56ac..95bbd8e 100644 --- a/DocGen4/Output/Find.lean +++ b/DocGen4/Output/Find.lean @@ -10,7 +10,7 @@ def find : HtmlM Html := do pure - + diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index d4f358f..05390fe 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -24,13 +24,15 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do - + + + diff --git a/static/declaration-data.js b/static/declaration-data.js new file mode 100644 index 0000000..ec72aa8 --- /dev/null +++ b/static/declaration-data.js @@ -0,0 +1,127 @@ +/** + * This module is a wrapper that facilitates manipulating the declaration data. + * + * Please see {@link DeclarationDataCenter} for more information. + */ + +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. + * + * *NOTE:* This is not made private to support legacy browsers. + */ + declarationData = []; + + /** + * Used to implement the singleton, in case we need to fetch data mutiple times in the same page. + */ + static singleton = null; + + /** + * Construct a DeclarationDataCenter with given data. + * + * Please use {@link DeclarationDataCenter.init} instead, which automates the data fetching process. + * @param {*} declarationData + */ + constructor(declarationData) { + this.declarationData = declarationData; + } + + /** + * The actual constructor of DeclarationDataCenter + * @returns {Promise} + */ + static async init() { + if (!DeclarationDataCenter.singleton) { + const dataUrl = new URL( + `${SITE_ROOT}declaration-data.bmp`, + window.location + ); + 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, + ]); + DeclarationDataCenter.singleton = new DeclarationDataCenter(data); + } + return DeclarationDataCenter.singleton; + } + + /** + * Search for a declaration. + * @returns {Array} + */ + search(pattern, strict = false) { + if (!pattern) { + return []; + } + // TODO: implement strict + return getMatches(this.declarationData, pattern); + } +} + +function isSeparater(char) { + return char === "." || char === "_"; +} + +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] + ) { + err += (isSeparater(pattern[j]) ? 0.125 : 1) * (i - lastMatch); + if (pattern[j] !== declName[i]) err += 0.5; + lastMatch = i + 1; + j++; + } else if (isSeparater(declName[i])) { + err += 0.125 * (i + 1 - lastMatch); + lastMatch = i + 1; + } + i++; + } + err += 0.125 * (declName.length - lastMatch); + if (j === pattern.length) { + return err; + } +} + +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); + // 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({ decl, err, link, source }); + } + } + 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 480f725..7fcb9ec 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -1,22 +1,28 @@ -import { SITE_ROOT } from "../site-root.js"; -import { declSearch } from "../search.js"; +/** + * This module is used for the `/find` endpoint. + */ -async function findRedirect(query, isSource) { - return declSearch(query).then((results) => { - window.location.replace(isSource? results[0].source : results[0].link); - }).catch(() => { +import { SITE_ROOT } from "../site-root.js"; +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 splits = window.location.href.split("#"); +let hash = window.location.hash.split("#"); -if (splits.length < 2) { +if (hash.length == 0) { window.location.replace(`${SITE_ROOT}/404.html`); } -if (splits[1].endsWith("/src")) { - findRedirect(splits[1].replace("/src", ""), true); +if (hash[1].endsWith("/src")) { + findRedirect(hash.replace("/src", ""), true); } else { - findRedirect(splits[1], false); + findRedirect(hash, false); } diff --git a/static/how-about.js b/static/how-about.js new file mode 100644 index 0000000..421f6e4 --- /dev/null +++ b/static/how-about.js @@ -0,0 +1,35 @@ +/** + * This module implements the `howabout` functionality in the 404 page. + */ + +import { DeclarationDataCenter } from "./declaration-data.js"; + +const HOW_ABOUT = document.querySelector("#howabout"); + +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 = + window.location.href.replace(/[/]/g, "/\u200b"); + + // 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; + } + } 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"; + } + }); +} diff --git a/static/mathjax-config.js b/static/mathjax-config.js index 9e470bc..076dbf6 100644 --- a/static/mathjax-config.js +++ b/static/mathjax-config.js @@ -1,26 +1,41 @@ /* - * This file is for configing MathJax behavior. - * Seehttps://docs.mathjax.org/en/latest/web/configuration.html - */ - -/** + * This file is for configing MathJax behavior. + * See https://docs.mathjax.org/en/latest/web/configuration.html + * * This configuration is copied from old doc-gen3 * https://github.com/leanprover-community/doc-gen */ MathJax = { tex: { - inlineMath: [['$', '$']], - displayMath: [['$$', '$$']] + inlineMath: [["$", "$"]], + displayMath: [["$$", "$$"]], }, options: { skipHtmlTags: [ - 'script', 'noscript', 'style', 'textarea', 'pre', - 'code', 'annotation', 'annotation-xml', - 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name', - 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields', - 'constructor', 'constructors', 'instances' + "script", + "noscript", + "style", + "textarea", + "pre", + "code", + "annotation", + "annotation-xml", + "decl", + "decl_meta", + "attributes", + "decl_args", + "decl_header", + "decl_name", + "decl_type", + "equation", + "equations", + "structure_field", + "structure_fields", + "constructor", + "constructors", + "instances", ], - ignoreHtmlClass: 'tex2jax_ignore', - processHtmlClass: 'tex2jax_process', + ignoreHtmlClass: "tex2jax_ignore", + processHtmlClass: "tex2jax_process", }, -}; \ No newline at end of file +}; diff --git a/static/nav.js b/static/nav.js index 3889da3..ff8404e 100644 --- a/static/nav.js +++ b/static/nav.js @@ -1,232 +1,43 @@ -import { declSearch } from "./search.js"; - -// Persistent expansion cookie for the file tree -// --------------------------------------------- +/** + * This module is used to implement persistent navbar expansion. + */ +// The variable to store the expansion information. let expanded = {}; -for (const e of (sessionStorage.getItem('expanded') || '').split(',')) { - if (e !== '') { + +// Load expansion information from sessionStorage. +for (const e of (sessionStorage.getItem("expanded") || "").split(",")) { + if (e !== "") { expanded[e] = true; } } +/** + * Save expansion information to sessionStorage. + */ function saveExpanded() { - sessionStorage.setItem("expanded", - Object.getOwnPropertyNames(expanded).filter((e) => expanded[e]).join(",")); + sessionStorage.setItem( + "expanded", + Object.getOwnPropertyNames(expanded) + .filter((e) => expanded[e]) + .join(",") + ); } -for (const elem of document.getElementsByClassName('nav_sect')) { - const id = elem.getAttribute('data-path'); +// save expansion information when user change the expansion. +for (const elem of document.getElementsByClassName("nav_sect")) { + const id = elem.getAttribute("data-path"); if (!id) continue; if (expanded[id]) { elem.open = true; } - elem.addEventListener('toggle', () => { + elem.addEventListener("toggle", () => { expanded[id] = elem.open; saveExpanded(); }); } -for (const currentFileLink of document.getElementsByClassName('visible')) { - currentFileLink.scrollIntoView({block: 'center'}); -} - - - - - - -// Tactic list tag filter -// ---------------------- - -function filterSelectionClass(tagNames, classname) { - if (tagNames.length == 0) { - for (const elem of document.getElementsByClassName(classname)) { - elem.classList.remove("hide"); - } - } else { - // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected - for (const elem of document.getElementsByClassName(classname)) { - elem.classList.add("hide"); - for (const tagName of tagNames) { - if (elem.classList.contains(tagName)) { - elem.classList.remove("hide"); - } - } - } - } - } - - function filterSelection(c) { - filterSelectionClass(c, "tactic"); - filterSelectionClass(c, "taclink"); - } - -var filterBoxes = document.getElementsByClassName("tagfilter"); - -function updateDisplay() { - filterSelection(getSelectValues()); -} - -function getSelectValues() { - var result = []; - - for (const opt of filterBoxes) { - - if (opt.checked) { - result.push(opt.value); - } - } - return result; - } - -function setSelectVal(val) { - for (const opt of filterBoxes) { - opt.checked = val; - } -} - -updateDisplay(); - -for (const opt of filterBoxes) { - opt.addEventListener('change', updateDisplay); -} - -const tse = document.getElementById("tagfilter-selectall") -if (tse != null) { - tse.addEventListener('change', function() { - setSelectVal(this.checked); - updateDisplay(); - }); -} - - - - - - -// Simple declaration search -// ------------------------- - -const srId = 'search_results'; -document.getElementById('search_form') - .appendChild(document.createElement('div')) - .id = srId; - -function handleSearchCursorUpDown(down) { - const sel = document.querySelector(`#${srId} .selected`); - const sr = document.getElementById(srId); - if (sel) { - sel.classList.remove('selected'); - const toSelect = down ? - sel.nextSibling || sr.firstChild: - sel.previousSibling || sr.lastChild; - toSelect && toSelect.classList.add('selected'); - } else { - const toSelect = down ? sr.firstChild : sr.lastChild; - toSelect && toSelect.classList.add('selected'); - } -} - -function handleSearchEnter() { - const sel = document.querySelector(`#${srId} .selected`) - || document.getElementById(srId).firstChild; - sel.click(); -} - -const searchInput = document.querySelector('#search_form input[name=q]'); - -searchInput.addEventListener('keydown', (ev) => { - switch (ev.key) { - case 'Down': - case 'ArrowDown': - ev.preventDefault(); - handleSearchCursorUpDown(true); - break; - case 'Up': - case 'ArrowUp': - ev.preventDefault(); - handleSearchCursorUpDown(false); - break; - case 'Enter': - ev.preventDefault(); - handleSearchEnter(); - break; - } -}); - -searchInput.addEventListener('input', async (ev) => { - const text = ev.target.value; - - if (!text) { - const sr = document.getElementById(srId); - sr.removeAttribute('state'); - sr.replaceWith(sr.cloneNode(false)); - return; - } - - document.getElementById(srId).setAttribute('state', 'loading'); - - const result = await declSearch(text); - if (ev.target.value != text) return; - - const oldSR = document.getElementById('search_results'); - const sr = oldSR.cloneNode(false); - for (const {decl, link} of result) { - const d = sr.appendChild(document.createElement('a')); - d.innerText = decl; - d.title = decl; - d.href = link; - } - sr.setAttribute('state', 'done'); - oldSR.replaceWith(sr); -}); - - - - - - -// 404 page goodies -// ---------------- - -const howabout = document.getElementById('howabout'); -if (howabout) { - howabout.innerText = "Please wait a second. I'll try to help you."; - - howabout.parentNode - .insertBefore(document.createElement('pre'), howabout) - .appendChild(document.createElement('code')) - .innerText = window.location.href.replace(/[/]/g, '/\u200b'); - - const query = window.location.href.match(/[/]([^/]+)(?:\.html|[/])?$/)[1]; - declSearch(query).then((results) => { - howabout.innerText = 'How about one of these instead:'; - const ul = howabout.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; - } - }); -} - - - - - - -// Rewrite GitHub links -// -------------------- - -for (const elem of document.getElementsByClassName('gh_link')) { - const a = elem.firstElementChild; - // commit is set in add_commit.js - for (const [prefix, replacement] of commit) { - if (a.href.startsWith(prefix)) { - a.href = a.href.replace(prefix, replacement); - break; - } - } -} +// Scroll to center. +for (const currentFileLink of document.getElementsByClassName("visible")) { + currentFileLink.scrollIntoView({ block: "center" }); +} \ No newline at end of file diff --git a/static/search.js b/static/search.js index 3449036..a6a72ea 100644 --- a/static/search.js +++ b/static/search.js @@ -1,67 +1,104 @@ -import { SITE_ROOT } from "./site-root.js"; +/** + * This module is used to handle user's interaction with the search form. + */ -function isSep(c) { - return c === '.' || c === '_'; -} +import { DeclarationDataCenter } from "./declaration-data.js"; -function matchCaseSensitive(declName, lowerDeclName, pat) { - let i = 0, j = 0, err = 0, lastMatch = 0 - while (i < declName.length && j < pat.length) { - if (pat[j] === declName[i] || pat[j] === lowerDeclName[i]) { - err += (isSep(pat[j]) ? 0.125 : 1) * (i - lastMatch); - if (pat[j] !== declName[i]) err += 0.5; - lastMatch = i + 1; - j++; - } else if (isSep(declName[i])) { - err += 0.125 * (i + 1 - lastMatch); - lastMatch = i + 1; - } - i++; - } - err += 0.125 * (declName.length - lastMatch); - if (j === pat.length) { - return err; - } -} -export function loadDecls(searchableDataCnt) { - return searchableDataCnt.map(({name, description, link, source}) => [name, name.toLowerCase(), description.toLowerCase(), link, source]); -} +const SEARCH_FORM = document.querySelector("#search_form"); +const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]"); -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, link, source] of decls) { - let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces); +// Create an `div#search_results` to hold all search results. +let sr = document.createElement("div"); +sr.id = "search_results"; +SEARCH_FORM.appendChild(sr); - // match all words as substrings of docstring - if (!(err < 3) && pat.length > 3 && lowerPats.every(l => lowerDoc.indexOf(l) != -1)) { - err = 3; - } - - if (err !== undefined) { - results.push({decl, err, link, source}); - } - } - return results.sort(({err: a}, {err: b}) => a - b).slice(0, maxResults); -} - -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; +/** + * Attach `selected` class to the the selected search result. + */ +function handleSearchCursorUpDown(down) { + const sel = sr.querySelector(`.selected`); + if (sel) { + sel.classList.remove("selected"); + const toSelect = down + ? sel.nextSibling || sr.firstChild + : sel.previousSibling || sr.lastChild; + toSelect && toSelect.classList.add("selected"); + } else { + const toSelect = down ? sr.firstChild : sr.lastChild; + toSelect && toSelect.classList.add("selected"); } -})() +} -export const declSearch = async (q) => getMatches(await getDecls(), q); \ No newline at end of file +/** + * Perform search (when enter is pressed). + */ +function handleSearchEnter() { + const sel = + sr.querySelector(`.selected`) || + sr.firstChild; + sel.click(); +} + +/** + * Allow user to navigate search results with up/down arrow keys, and choose with enter. + */ +SEARCH_INPUT.addEventListener("keydown", (ev) => { + switch (ev.key) { + case "Down": + case "ArrowDown": + ev.preventDefault(); + handleSearchCursorUpDown(true); + break; + case "Up": + case "ArrowUp": + ev.preventDefault(); + handleSearchCursorUpDown(false); + break; + case "Enter": + ev.preventDefault(); + handleSearchEnter(); + break; + } +}); + +/** + * Remove all children of a DOM node. + */ +function removeAllChildren(node) { + while (node.firstChild) { + node.removeChild(node.lastChild); + } +} + +/** + * Search autocompletion. + */ +SEARCH_INPUT.addEventListener("input", async (ev) => { + const text = ev.target.value; + + // If no input clear all. + if (!text) { + sr.removeAttribute("state"); + removeAllChildren(sr); + return; + } + + // searching + sr.setAttribute("state", "loading"); + const dataCenter = await DeclarationDataCenter.init(); + const result = dataCenter.search(text); + + // in case user has updated the input. + if (ev.target.value != text) return; + + // update search results + removeAllChildren(sr); + for (const { decl, link } of result) { + const d = sr.appendChild(document.createElement("a")); + d.innerText = decl; + d.title = decl; + d.href = link; + } + sr.setAttribute("state", "done"); +}); diff --git a/static/site-root.js b/static/site-root.js index 0663d6b..3dd39a3 100644 --- a/static/site-root.js +++ b/static/site-root.js @@ -1 +1,4 @@ +/** + * Get the site root, {siteRoot} is to be replaced by doc-gen4. + */ export const SITE_ROOT = "{siteRoot}"; \ No newline at end of file diff --git a/static/tactic.js b/static/tactic.js new file mode 100644 index 0000000..e40c4ec --- /dev/null +++ b/static/tactic.js @@ -0,0 +1,61 @@ +// TODO: The tactic part seem to be unimplemented now. + +function filterSelectionClass(tagNames, classname) { + if (tagNames.length == 0) { + for (const elem of document.getElementsByClassName(classname)) { + elem.classList.remove("hide"); + } + } else { + // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected + for (const elem of document.getElementsByClassName(classname)) { + elem.classList.add("hide"); + for (const tagName of tagNames) { + if (elem.classList.contains(tagName)) { + elem.classList.remove("hide"); + } + } + } + } +} + +function filterSelection(c) { + filterSelectionClass(c, "tactic"); + filterSelectionClass(c, "taclink"); +} + +var filterBoxes = document.getElementsByClassName("tagfilter"); + +function updateDisplay() { + filterSelection(getSelectValues()); +} + +function getSelectValues() { + var result = []; + + for (const opt of filterBoxes) { + if (opt.checked) { + result.push(opt.value); + } + } + return result; +} + +function setSelectVal(val) { + for (const opt of filterBoxes) { + opt.checked = val; + } +} + +updateDisplay(); + +for (const opt of filterBoxes) { + opt.addEventListener("change", updateDisplay); +} + +const tse = document.getElementById("tagfilter-selectall"); +if (tse != null) { + tse.addEventListener("change", function () { + setSelectVal(this.checked); + updateDisplay(); + }); +} From 004977e6e42a7e64cef61f860c53a2a40dcb5569 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Tue, 22 Feb 2022 15:01:14 +0800 Subject: [PATCH 11/23] refactor: use strict match for find --- DocGen4/Output.lean | 4 +-- static/declaration-data.js | 67 ++++++++++++++++++++++---------------- static/find/find.js | 20 +++++------- static/how-about.js | 36 +++++++++++--------- 4 files changed, 70 insertions(+), 57 deletions(-) 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"; - } - }); + }); + } } From e4ccc5cf50883b8ae3d468e19cea356c88c76a13 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Tue, 22 Feb 2022 23:20:20 +0800 Subject: [PATCH 12/23] feat: add browser cache for data fix search name --- static/declaration-data.js | 129 ++++++++++++++++++++++++++++++++----- static/search.js | 6 +- 2 files changed, 117 insertions(+), 18 deletions(-) diff --git a/static/declaration-data.js b/static/declaration-data.js index 0d07024..0cdc869 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -6,6 +6,9 @@ import { SITE_ROOT } from "./site-root.js"; +const CACHE_DB_NAME = "declaration-data"; +const CACHE_DB_VERSION = 1; + /** * The DeclarationDataCenter is used for declaration searching. * @@ -40,26 +43,46 @@ export class DeclarationDataCenter { */ static async init() { if (!DeclarationDataCenter.singleton) { + const timestampUrl = new URL( + `${SITE_ROOT}declaration-data.timestamp`, + window.location + ); const dataUrl = new URL( `${SITE_ROOT}declaration-data.bmp`, window.location ); - const response = await fetch(dataUrl); - const json = await response.json(); - // the data is a map of name (original case) to declaration data. - const data = new Map( - json.map(({ name, doc, link, source: sourceLink }) => [ - name, - { + + const timestampRes = await fetch(timestampUrl); + const timestamp = await timestampRes.text(); + + // try to use cache first + let store = await getDeclarationStore(); + const data = await fetchCachedDeclarationData(store, timestamp); + if (data) { + // if data is defined, use the cached one. + DeclarationDataCenter.singleton = new DeclarationDataCenter(data); + } else { + // undefined. then fetch the data from the server. + const dataRes = await fetch(dataUrl); + const dataJson = await dataRes.json(); + // the data is a map of name (original case) to declaration data. + const data = new Map( + dataJson.map(({ name, doc, link, source: sourceLink }) => [ name, - lowerName: name.toLowerCase(), - lowerDoc: doc.toLowerCase(), - link, - sourceLink, - }, - ]) - ); - DeclarationDataCenter.singleton = new DeclarationDataCenter(data); + { + name, + lowerName: name.toLowerCase(), + lowerDoc: doc.toLowerCase(), + link, + sourceLink, + }, + ]) + ); + // get store again in case it's inactive + let store = await getDeclarationStore(); + await cacheDeclarationData(store, timestamp, data); + DeclarationDataCenter.singleton = new DeclarationDataCenter(data); + } } return DeclarationDataCenter.singleton; } @@ -136,3 +159,79 @@ function getMatches(declarations, pattern, maxResults = 30) { } return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults); } + +// TODO: refactor the indexedDB part to be more robust + +/** + * Get the indexedDB database, automatically initialized. + * @returns {Promise} + */ +function getDeclarationStore() { + return new Promise((resolve, reject) => { + const request = indexedDB.open(CACHE_DB_NAME, CACHE_DB_VERSION); + request.onerror = function (event) { + reject( + new Error( + `fail to open indexedDB ${CACHE_DB_NAME} of version ${CACHE_DB_VERSION}` + ) + ); + }; + request.onupgradeneeded = function (event) { + let db = event.target.result; + // We only need to store one object, so no key path or increment is needed. + let objectStore = db.createObjectStore("declaration"); + objectStore.transaction.oncomplete = function (event) { + resolve(objectStore); + }; + }; + request.onsuccess = function (event) { + resolve( + event.target.result + .transaction("declaration", "readwrite") + .objectStore("declaration") + ); + }; + }); +} + +/** + * Store data in indexedDB object store. + * @param {IDBObjectStore} store + * @param {string} timestamp + * @param {Map} data + */ +function cacheDeclarationData(store, timestamp, data) { + return new Promise((resolve, reject) => { + let clearRequest = store.clear(); + clearRequest.onsuccess = function (event) { + let addRequest = store.add(data, timestamp); + addRequest.onsuccess = function (event) { + resolve(); + }; + addRequest.onerror = function (event) { + reject(new Error(`fail to store declaration data`)); + }; + }; + clearRequest.onerror = function (event) { + reject(new Error("fail to clear object store")); + }; + }); +} + +/** + * Retrieve data from indexedDB database. + * @param {IDBObjectStore} store + * @param {string} timestamp + * @returns {Promise|undefined>} + */ +async function fetchCachedDeclarationData(store, timestamp) { + return new Promise((resolve, reject) => { + let transactionRequest = store.get(timestamp); + transactionRequest.onsuccess = function (event) { + resolve(event.result); + }; + transactionRequest.onerror = function (event) { + reject(new Error(`fail to store declaration data`)); + }; + }); +} diff --git a/static/search.js b/static/search.js index a6a72ea..d5e2fb6 100644 --- a/static/search.js +++ b/static/search.js @@ -94,10 +94,10 @@ SEARCH_INPUT.addEventListener("input", async (ev) => { // update search results removeAllChildren(sr); - for (const { decl, link } of result) { + for (const { name, link } of result) { const d = sr.appendChild(document.createElement("a")); - d.innerText = decl; - d.title = decl; + d.innerText = name; + d.title = name; d.href = link; } sr.setAttribute("state", "done"); From a18e3438294ab688d3a255a548f4eaff44839b33 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Wed, 23 Feb 2022 04:26:20 +0800 Subject: [PATCH 13/23] refactor: change find syntax --- DocGen4/Output.lean | 14 +++++-- DocGen4/Output/Semantic.lean | 58 +++++++++++++++++++++++++++ static/declaration-data.js | 8 ++-- static/find/find.js | 76 +++++++++++++++++++++++++++++------- static/how-about.js | 6 +-- static/search.js | 6 +-- 6 files changed, 141 insertions(+), 27 deletions(-) create mode 100644 DocGen4/Output/Semantic.lean diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index ae4d03a..21ebb15 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -10,6 +10,7 @@ import DocGen4.Output.Index import DocGen4.Output.Module import DocGen4.Output.NotFound import DocGen4.Output.Find +import DocGen4.Output.Semantic namespace DocGen4 @@ -69,19 +70,24 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let notFoundHtml := ReaderT.run notFound config FS.createDirAll basePath FS.createDirAll (basePath / "find") + FS.createDirAll (basePath / "semantic") let mut declList := #[] for (_, mod) in result.moduleInfo.toArray do for decl in filterMapDocInfo mod.members do let name := decl.getName.toString 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), ("doc", doc), ("link", link), ("source", source)] + let link := root ++ s!"semantic/{decl.getName.hash}.xml#" + let docLink := Id.run <| ReaderT.run (declNameToLink decl.getName) config + let sourceLink := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config + let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourcLink", sourceLink)] declList := declList.push obj - + let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config + FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml let json := Json.arr declList + FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config + FS.writeFile (basePath / "index.html") indexHtml.toString FS.writeFile (basePath / "404.html") notFoundHtml.toString FS.writeFile (basePath / "find" / "index.html") findHtml.toString diff --git a/DocGen4/Output/Semantic.lean b/DocGen4/Output/Semantic.lean new file mode 100644 index 0000000..7b22cdf --- /dev/null +++ b/DocGen4/Output/Semantic.lean @@ -0,0 +1,58 @@ +import DocGen4.Output.Template +import DocGen4.Output.DocString +import Lean.Data.Xml + +open Lean Xml + +namespace DocGen4 +namespace Output + +instance : ToString $ Array Element where + toString xs := xs.map toString |>.foldl String.append "" + +instance : Coe Element Content where + coe e := Content.Element e + +-- TODO: syntax metaprogramming and basic semantic data + +def semanticXml (i : DocInfo) : HtmlM $ Array Element := do + pure #[ + Element.Element + "rdf:RDF" + (Std.RBMap.fromList [ + ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"), + ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#") + ] _) + #[ + Element.Element + "rdf:Description" + (Std.RBMap.fromList [ + ("rdf:about", s!"{←getRoot}semactic/{i.getName.hash}.xml#") + ] _) + #[] + ] + ] + +def schemaXml : HtmlM $ Array Element := do + pure #[ + Element.Element + "rdf:RDF" + (Std.RBMap.fromList [ + ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"), + ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#") + ] _) + #[ + Element.Element + "docgen4:hasInstance" + Std.RBMap.empty + #[ + Element.Element + "rdfs:type" + Std.RBMap.empty + #[Content.Character "rdf:Property"] + ] + ] + ] + +end Output +end DocGen4 diff --git a/static/declaration-data.js b/static/declaration-data.js index 0cdc869..2439e4a 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -67,13 +67,14 @@ export class DeclarationDataCenter { const dataJson = await dataRes.json(); // the data is a map of name (original case) to declaration data. const data = new Map( - dataJson.map(({ name, doc, link, source: sourceLink }) => [ + dataJson.map(({ name, doc, link, docLink, sourceLink }) => [ name, { name, lowerName: name.toLowerCase(), lowerDoc: doc.toLowerCase(), link, + docLink, sourceLink, }, ]) @@ -91,7 +92,7 @@ export class DeclarationDataCenter { * Search for a declaration. * @returns {Array} */ - search(pattern, strict = false) { + search(pattern, strict = true) { if (!pattern) { return []; } @@ -142,6 +143,7 @@ function getMatches(declarations, pattern, maxResults = 30) { lowerName, lowerDoc, link, + docLink, sourceLink, } of declarations.values()) { let err = matchCaseSensitive(name, lowerName, patNoSpaces); @@ -154,7 +156,7 @@ function getMatches(declarations, pattern, maxResults = 30) { err = 3; } if (err !== undefined) { - results.push({ name, err, lowerName, lowerDoc, link, sourceLink }); + results.push({ name, err, lowerName, lowerDoc, link, docLink, 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 75b5507..597ed38 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -1,26 +1,74 @@ /** * This module is used for the `/find` endpoint. + * + * Two basic kinds of search syntax are supported: + * + * 1. Query-Fragment syntax: `/find?pattern=Nat.add#doc` for documentation and `/find?pattern=Nat.add#src` for source code. + * 2. Fragment-Only syntax:`/find/#doc/Nat.add` for documentation and `/find/#src/Nat.add` for source code. + * + * Though both of them are valid, the first one is highly recommended, and the second one is for compatibility and taste. + * + * There are some extended usage for the QF syntax. For example, appending `strict=false` to the query part + * (`/find?pattern=Nat.add&strict=false#doc`) will allow you to use the fuzzy search, rather than strict match. + * Also, the fragment is extensible as well. For now only `#doc` and `#src` are implement, and the plain query without + * hash (`/find?pattern=Nat.add`) is used for computer-friendly data (semantic web is great! :P), while all other fragments + * fallback to the `#doc` view. */ import { SITE_ROOT } from "../site-root.js"; import { DeclarationDataCenter } from "../declaration-data.js"; -async function findRedirect(pattern, isSource) { +/** + * We don't use browser's default hash and searchParams in case Lean declaration name + * can be like `«#»`, rather we manually handle the `window.location.href` with regex. + */ +const LEAN_FRIENDLY_URL_REGEX = /^[^?#]+(?:\?((?:[^«#»]|«.*»)*))?(?:#(.*))?$/; +const LEAN_FRIENDLY_AND_SEPARATOR = /(? p.split(LEAN_FRIENDLY_EQUAL_SEPARATOR)) + ?.filter((l) => l.length == 2 && l[0].length > 0) +); +const fragmentPaths = fragment?.split(LEAN_FRIENDLY_SLASH_SEPARATOR) ?? []; + +const pattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail then second, may be undefined +const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true +const view = fragmentPaths[0]; + +/** + * Find the result and redirect to the result page. + * @param {string} pattern the pattern to search for + * @param {string} view the view of the find result (`"doc"` or `"src"` for now) + */ +async function findAndRedirect(pattern, strict, view) { + // if no pattern provided, directly redirect to the 404 page + if (!pattern) { + window.location.replace(`${SITE_ROOT}404.html`); + } + // search for result const dataCenter = await DeclarationDataCenter.init(); - let results = dataCenter.search(pattern, true); - if (results.length == 0) { - // if there is no exact match, redirect to 404 page to use fuzzy match + let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array + // if no result found, redirect to the 404 page + if (!result) { + // TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found. window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`); } else { - // redirect to doc or source page. + // success, redirect to doc or source page, or to the semantic rdf. window.location.replace(isSource ? results[0].sourceLink : results[0].link); + if (!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); + } } -} - -let hash = window.location.hash.replace("#", ""); - -if (hash.endsWith("/src")) { - findRedirect(hash.replace("/src", ""), true); -} else { - findRedirect(hash, false); -} +} \ No newline at end of file diff --git a/static/how-about.js b/static/how-about.js index cb9832b..5c03ffd 100644 --- a/static/how-about.js +++ b/static/how-about.js @@ -20,14 +20,14 @@ if (HOW_ABOUT) { if (pattern) { HOW_ABOUT.innerText = "Please wait a second. I'll try to help you."; DeclarationDataCenter.init().then((dataCenter) => { - let results = dataCenter.search(pattern); + let results = dataCenter.search(pattern, false); 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) { + for (const { name, docLink } of results) { const li = ul.appendChild(document.createElement("li")); const a = li.appendChild(document.createElement("a")); - a.href = link; + a.href = docLink; a.appendChild(document.createElement("code")).innerText = name; } } else { diff --git a/static/search.js b/static/search.js index d5e2fb6..1df8690 100644 --- a/static/search.js +++ b/static/search.js @@ -87,18 +87,18 @@ SEARCH_INPUT.addEventListener("input", async (ev) => { // searching sr.setAttribute("state", "loading"); const dataCenter = await DeclarationDataCenter.init(); - const result = dataCenter.search(text); + const result = dataCenter.search(text, false); // in case user has updated the input. if (ev.target.value != text) return; // update search results removeAllChildren(sr); - for (const { name, link } of result) { + for (const { name, docLink } of result) { const d = sr.appendChild(document.createElement("a")); d.innerText = name; d.title = name; - d.href = link; + d.href = docLink; } sr.setAttribute("state", "done"); }); From 2b217ecda0fc0ed4679634784a4db1b3ed614dec Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Wed, 23 Feb 2022 05:32:37 +0800 Subject: [PATCH 14/23] fix: fix find search --- DocGen4/Output.lean | 2 +- static/declaration-data.js | 62 ++++++++++++++++++++------------------ static/find/find.js | 3 +- 3 files changed, 36 insertions(+), 31 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 21ebb15..7351530 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -80,7 +80,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let link := root ++ s!"semantic/{decl.getName.hash}.xml#" let docLink := Id.run <| ReaderT.run (declNameToLink decl.getName) config let sourceLink := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config - let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourcLink", sourceLink)] + let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourceLink", sourceLink)] declList := declList.push obj let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml diff --git a/static/declaration-data.js b/static/declaration-data.js index 2439e4a..cb7a90c 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -56,8 +56,7 @@ export class DeclarationDataCenter { const timestamp = await timestampRes.text(); // try to use cache first - let store = await getDeclarationStore(); - const data = await fetchCachedDeclarationData(store, timestamp); + const data = await fetchCachedDeclarationData(timestamp); if (data) { // if data is defined, use the cached one. DeclarationDataCenter.singleton = new DeclarationDataCenter(data); @@ -79,9 +78,7 @@ export class DeclarationDataCenter { }, ]) ); - // get store again in case it's inactive - let store = await getDeclarationStore(); - await cacheDeclarationData(store, timestamp, data); + await cacheDeclarationData(timestamp, data); DeclarationDataCenter.singleton = new DeclarationDataCenter(data); } } @@ -156,7 +153,15 @@ function getMatches(declarations, pattern, maxResults = 30) { err = 3; } if (err !== undefined) { - results.push({ name, err, lowerName, lowerDoc, link, docLink, sourceLink }); + results.push({ + name, + err, + lowerName, + lowerDoc, + link, + docLink, + sourceLink, + }); } } return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults); @@ -166,11 +171,12 @@ function getMatches(declarations, pattern, maxResults = 30) { /** * Get the indexedDB database, automatically initialized. - * @returns {Promise} + * @returns {Promise} */ -function getDeclarationStore() { +async function getDeclarationDatabase() { return new Promise((resolve, reject) => { const request = indexedDB.open(CACHE_DB_NAME, CACHE_DB_VERSION); + request.onerror = function (event) { reject( new Error( @@ -181,38 +187,33 @@ function getDeclarationStore() { request.onupgradeneeded = function (event) { let db = event.target.result; // We only need to store one object, so no key path or increment is needed. - let objectStore = db.createObjectStore("declaration"); - objectStore.transaction.oncomplete = function (event) { - resolve(objectStore); - }; + db.createObjectStore("declaration"); }; request.onsuccess = function (event) { - resolve( - event.target.result - .transaction("declaration", "readwrite") - .objectStore("declaration") - ); + resolve(event.target.result); }; }); } /** * Store data in indexedDB object store. - * @param {IDBObjectStore} store * @param {string} timestamp * @param {Map} data */ -function cacheDeclarationData(store, timestamp, data) { +async function cacheDeclarationData(timestamp, data) { + let db = await getDeclarationDatabase(); + let store = db + .transaction("declaration", "readwrite") + .objectStore("declaration"); return new Promise((resolve, reject) => { let clearRequest = store.clear(); - clearRequest.onsuccess = function (event) { - let addRequest = store.add(data, timestamp); - addRequest.onsuccess = function (event) { - resolve(); - }; - addRequest.onerror = function (event) { - reject(new Error(`fail to store declaration data`)); - }; + let addRequest = store.add(data, timestamp); + + addRequest.onsuccess = function (event) { + resolve(); + }; + addRequest.onerror = function (event) { + reject(new Error(`fail to store declaration data`)); }; clearRequest.onerror = function (event) { reject(new Error("fail to clear object store")); @@ -222,11 +223,14 @@ function cacheDeclarationData(store, timestamp, data) { /** * Retrieve data from indexedDB database. - * @param {IDBObjectStore} store * @param {string} timestamp * @returns {Promise|undefined>} */ -async function fetchCachedDeclarationData(store, timestamp) { +async function fetchCachedDeclarationData(timestamp) { + let db = await getDeclarationDatabase(); + let store = db + .transaction("declaration", "readonly") + .objectStore("declaration"); return new Promise((resolve, reject) => { let transactionRequest = store.get(timestamp); transactionRequest.onsuccess = function (event) { diff --git a/static/find/find.js b/static/find/find.js index 597ed38..4b65f26 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -40,6 +40,8 @@ const pattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true const view = fragmentPaths[0]; +findAndRedirect(pattern, strict, view); + /** * Find the result and redirect to the result page. * @param {string} pattern the pattern to search for @@ -59,7 +61,6 @@ async function findAndRedirect(pattern, strict, view) { window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`); } else { // success, redirect to doc or source page, or to the semantic rdf. - window.location.replace(isSource ? results[0].sourceLink : results[0].link); if (!view) { window.location.replace(result.link); } else if (view == "doc") { From a5dfba5f1ccc840a0946f7bd23d3c6bf8e133068 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Wed, 23 Feb 2022 23:09:10 +0800 Subject: [PATCH 15/23] fix: fix navbar centering --- DocGen4/Output/Navbar.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index efc9735..e56aa38 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -14,7 +14,7 @@ open Lean open scoped DocGen4.Jsx def moduleListFile (file : Name) : HtmlM Html := do - pure
+ pure From a50ca857aaf8219504f7b16154e891e950a2506a Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Wed, 23 Feb 2022 23:28:15 +0800 Subject: [PATCH 16/23] fix: wrap navbar overflow --- static/style.css | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/static/style.css b/static/style.css index a4e0c9a..d056b40 100644 --- a/static/style.css +++ b/static/style.css @@ -273,10 +273,15 @@ nav { margin-top: 1ex; } -.nav details, .nav_link { +.nav details > * { padding-left: 2ex; } +.nav summary { + cursor: pointer; + padding-left: 0; +} + .nav summary::marker { font-size: 85%; } @@ -294,6 +299,10 @@ nav { overflow-wrap: break-word; } +.nav_link { + overflow-wrap: break-word; +} + .decl > div, .mod_doc { padding-left: 8px; padding-right: 8px; From dca4e42665f6c4d126fcbe9fb993f7bdb3f2a495 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Wed, 23 Feb 2022 23:33:34 +0800 Subject: [PATCH 17/23] fix: filter out nonexist modules --- DocGen4/Output/Navbar.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index e56aa38..1a75288 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -29,7 +29,12 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do pure
- {Html.element "summary" true #[] #[{h.getName.toString}]} + { + if (←getResult).moduleInfo.contains h.getName then + Html.element "summary" true #[] #[{h.getName.toString}] + else + {h.getName.toString} + } [dirNodes] [fileNodes]
From 34d2239b68c948d8cc19a6cbd41c06b8b995930f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 23 Feb 2022 22:54:10 +0100 Subject: [PATCH 18/23] feat: actual CLI --- DocGen4/Load.lean | 8 ++++---- Main.lean | 28 +++++++++++++++++++--------- lakefile.lean | 4 ++++ 3 files changed, 27 insertions(+), 13 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 20da38a..d220389 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -20,15 +20,15 @@ def getLakePath : IO FilePath := do pure $ lakePath.withExtension System.FilePath.exeExtension -- Modified from the LSP Server -def lakeSetupSearchPath (lakePath : System.FilePath) (imports : Array String) : IO Lean.SearchPath := do - let args := #["print-paths"] ++ imports - let cmdStr := " ".intercalate (toString lakePath :: args.toList) +def lakeSetupSearchPath (lakePath : System.FilePath) (imports : List String) : IO Lean.SearchPath := do + let args := "print-paths" :: imports + let cmdStr := " ".intercalate (toString lakePath :: args) let lakeProc ← Process.spawn { stdin := Process.Stdio.null stdout := Process.Stdio.piped stderr := Process.Stdio.piped cmd := lakePath.toString - args + args := args.toArray } let stdout := String.trim (← lakeProc.stdout.readToEnd) let stderr := String.trim (← lakeProc.stderr.readToEnd) diff --git a/Main.lean b/Main.lean index 13e530b..4a7c71d 100644 --- a/Main.lean +++ b/Main.lean @@ -1,17 +1,27 @@ import DocGen4 import Lean +import Cli -open DocGen4 Lean IO +open DocGen4 Lean Cli -def main (args : List String) : IO Unit := do - if args.isEmpty then - IO.println "Usage: doc-gen4 root/url/ Module1 Module2 ..." - IO.Process.exit 1 - return - let root := args.head! - let modules := args.tail! - let path ← lakeSetupSearchPath (←getLakePath) modules.toArray +def runDocGenCmd (p : Parsed) : IO UInt32 := do + let root := p.positionalArg! "root" |>.as! String + let modules : List String := p.variableArgsAs! String |>.toList + let path ← lakeSetupSearchPath (←getLakePath) modules IO.println s!"Loading modules from: {path}" let doc ← load $ modules.map Name.mkSimple IO.println "Outputting HTML" htmlOutput doc root + pure 0 + +def docGenCmd : Cmd := `[Cli| + "doc-gen4" VIA runDocGenCmd; ["0.0.1"] + "A documentation generator for Lean 4." + + ARGS: + root : String; "The root URL to generate the HTML for (will be relative in the future)" + ...modules : String; "The modules to generate the HTML for" +] + +def main (args : List String) : IO UInt32 := + docGenCmd.validate args diff --git a/lakefile.lean b/lakefile.lean index cc8dd0e..9d9c138 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,6 +12,10 @@ package «doc-gen4» { { name := `Unicode src := Source.git "https://github.com/xubaiw/Unicode.lean" "3b7b85472d42854a474099928a3423bb97d4fa64" + }, + { + name := `Cli + src := Source.git "https://github.com/mhuisi/lean4-cli" "1f8663e3dafdcc11ff476d74ef9b99ae5bdaedd3" } ] } From 5f7d380ab75179959fe39b441c77e7e8d18c48ea Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sat, 26 Feb 2022 09:41:25 +0800 Subject: [PATCH 19/23] refactor: make include_str relative to file --- DocGen4/IncludeStr.lean | 34 ++++++++++++++++++++++++++++++---- DocGen4/Output/Base.lean | 16 ++++++++-------- 2 files changed, 38 insertions(+), 12 deletions(-) diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean index 511a181..afc3ceb 100644 --- a/DocGen4/IncludeStr.lean +++ b/DocGen4/IncludeStr.lean @@ -7,13 +7,37 @@ import Lean namespace DocGen4 -open Lean System IO Lean.Elab.Term +open Lean System IO Lean.Elab.Term FS + +deriving instance DecidableEq for FileType + +/-- + Traverse all subdirectories fo `f` to find if one satisfies `p`. +-/ +partial def traverseDir (f : FilePath) (p : FilePath → IO Bool) : IO (Option FilePath) := do + if (← p f) then + return f + for d in (← System.FilePath.readDir f) do + let subDir := d.path + let metadata ← subDir.metadata + if metadata.type = FileType.dir then + if let some p ← traverseDir subDir p then + return p + return none syntax (name := includeStr) "include_str" str : term @[termElab includeStr] def includeStrImpl : TermElab := λ stx expectedType? => do - let str := stx[1].isStrLit?.get! - let path := FilePath.mk str + let str := stx[1].isStrLit?.get! + let srcPath := (FilePath.mk (← read).fileName) + let currentDir ← IO.currentDir + -- HACK: Currently we cannot get current file path in VSCode, we have to traversely find the matched subdirectory in the current directory. + if let some path ← match srcPath.parent with + | some p => pure $ some $ p / str + | none => do + let foundDir ← traverseDir currentDir λ p => p / str |>.pathExists + pure $ foundDir.map (· / str) + then if ←path.pathExists then if ←path.isDir then throwError s!"{str} is a directory" @@ -21,6 +45,8 @@ syntax (name := includeStr) "include_str" str : term let content ← FS.readFile path pure $ mkStrLit content else - throwError s!"\"{str}\" does not exist as a file" + throwError s!"{path} does not exist as a file" + else + throwError s!"No such file in whole directory: {str}" end DocGen4 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 2a28b17..2f84500 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -46,14 +46,14 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := basePath / parts.foldl (· / ·) (FilePath.mk ".") section Static - def styleCss : String := include_str "./static/style.css" - def siteRootJs : String := include_str "./static/site-root.js" - def declarationDataCenterJs : String := include_str "./static/declaration-data.js" - def navJs : String := include_str "./static/nav.js" - def howAboutJs : String := include_str "./static/how-about.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" + def styleCss : String := include_str "../../static/style.css" + def siteRootJs : String := include_str "../../static/site-root.js" + def declarationDataCenterJs : String := include_str "../../static/declaration-data.js" + def navJs : String := include_str "../../static/nav.js" + def howAboutJs : String := include_str "../../static/how-about.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 def declNameToLink (name : Name) : HtmlM String := do From 6492f827b7f4af35b046b5b53c91b18a39b365d6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 27 Feb 2022 18:01:34 +0100 Subject: [PATCH 20/23] chore: bump toolchain --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 7c2b6c2..abadd14 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-02-17 +leanprover/lean4:nightly-2022-02-27 From 55356167253c83a749d99eebd0e171d9c802eb50 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 6 Mar 2022 16:48:49 +0100 Subject: [PATCH 21/23] chore: Bump toolchain --- DocGen4/Load.lean | 4 ++-- lean-toolchain | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index d220389..e49f23b 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -16,7 +16,7 @@ def getLakePath : IO FilePath := do match (← IO.getEnv "LAKE") with | some path => pure $ System.FilePath.mk path | none => - let lakePath := (←findSysroot?) / "bin" / "lake" + let lakePath := (←findSysroot) / "bin" / "lake" pure $ lakePath.withExtension System.FilePath.exeExtension -- Modified from the LSP Server @@ -37,7 +37,7 @@ def lakeSetupSearchPath (lakePath : System.FilePath) (imports : List String) : I let stdout := stdout.split (· == '\n') |>.getLast! let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?) | throw $ userError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}" - initSearchPath (← findSysroot?) paths.oleanPath + initSearchPath (← findSysroot) paths.oleanPath paths.oleanPath.mapM realPathNormalized | 2 => pure [] -- no lakefile.lean | _ => throw $ userError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}" diff --git a/lean-toolchain b/lean-toolchain index abadd14..8e380ba 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-02-27 +leanprover/lean4:nightly-2022-03-06 From 9cc4c787e6e90f6838bafeb040b6b337c83b9c3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 6 Mar 2022 18:51:06 +0100 Subject: [PATCH 22/23] feat: lake integration --- DocGen4/Load.lean | 46 ++++++++++++++------------------------ DocGen4/Output.lean | 54 ++++++++++++++++++++++++++++++--------------- Main.lean | 15 ++++++++----- lakefile.lean | 4 ++++ 4 files changed, 65 insertions(+), 54 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index e49f23b..841891a 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -5,6 +5,7 @@ Authors: Henrik Böving -/ import Lean +import Lake import DocGen4.Process import Std.Data.HashMap @@ -12,40 +13,25 @@ namespace DocGen4 open Lean System Std IO -def getLakePath : IO FilePath := do - match (← IO.getEnv "LAKE") with - | some path => pure $ System.FilePath.mk path - | none => - let lakePath := (←findSysroot) / "bin" / "lake" - pure $ lakePath.withExtension System.FilePath.exeExtension - --- Modified from the LSP Server -def lakeSetupSearchPath (lakePath : System.FilePath) (imports : List String) : IO Lean.SearchPath := do - let args := "print-paths" :: imports - let cmdStr := " ".intercalate (toString lakePath :: args) - let lakeProc ← Process.spawn { - stdin := Process.Stdio.null - stdout := Process.Stdio.piped - stderr := Process.Stdio.piped - cmd := lakePath.toString - args := args.toArray - } - let stdout := String.trim (← lakeProc.stdout.readToEnd) - let stderr := String.trim (← lakeProc.stderr.readToEnd) - match (← lakeProc.wait) with - | 0 => - let stdout := stdout.split (· == '\n') |>.getLast! - let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?) - | throw $ userError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}" - initSearchPath (← findSysroot) paths.oleanPath - paths.oleanPath.mapM realPathNormalized - | 2 => pure [] -- no lakefile.lean - | _ => throw $ userError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}" +def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do + let (leanInstall?, lakeInstall?) ← Lake.findInstall? + let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO' + match res with + | Except.ok (ws, options) => + let lean := leanInstall?.get! + if lean.githash ≠ Lean.githash then + IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {lean.githash}" + let lake := lakeInstall?.get! + let ctx ← Lake.mkBuildContext ws lean lake + ws.root.buildImportsAndDeps imports |>.run Lake.LogMethods.eio ctx + initSearchPath (←findSysroot) ws.leanPaths.oleanPath + pure $ Except.ok (ws, lean.githash) + | Except.error rc => pure $ Except.error rc def load (imports : List Name) : IO AnalyzerResult := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty -- TODO parameterize maxHeartbeats IO.println "Processing modules" - Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}) + Prod.fst <$> Meta.MetaM.toIO process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {} end DocGen4 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 7351530..4412ec5 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ import Lean +import Lake import DocGen4.Process import DocGen4.Output.Base import DocGen4.Output.Index @@ -25,12 +26,8 @@ Three link types from git supported: TODO: This function is quite brittle and very github specific, we can probably do better. -/ -def getGithubBaseUrl : IO String := do - let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]} - if out.exitCode != 0 then - throw <| IO.userError <| "git exited with code " ++ toString out.exitCode - let mut url := out.stdout.trimRight - +def getGithubBaseUrl (gitUrl : String) : String := Id.run do + let mut url := gitUrl if url.startsWith "git@" then url := url.drop 15 url := url.dropRight 4 @@ -40,30 +37,51 @@ def getGithubBaseUrl : IO String := do else pure url -def getCommit : IO String := do +def getProjectGithubUrl : IO String := do + let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]} + if out.exitCode != 0 then + throw <| IO.userError <| "git exited with code " ++ toString out.exitCode + pure out.stdout.trimRight + +def getProjectCommit : IO String := do let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]} if out.exitCode != 0 then throw <| IO.userError <| "git exited with code " ++ toString out.exitCode pure out.stdout.trimRight -def sourceLinker : IO (Name → Option DeclarationRange → String) := do - let baseUrl ← getGithubBaseUrl - let commit ← getCommit - pure λ name range => - let parts := name.components.map Name.toString +def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do + -- Compute a map from package names to source URL + let mut gitMap := Std.mkHashMap + let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl) + let projectCommit ← getProjectCommit + gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit) + for pkg in ws.packageArray do + for dep in pkg.dependencies do + let value := match dep.src with + | Lake.Source.git url commit => (getGithubBaseUrl url, commit) + -- TODO: What do we do here if linking a source is not possible? + | _ => ("https://example.com", "master") + gitMap := gitMap.insert dep.name value + + pure $ λ module range => + let parts := module.components.map Name.toString let path := (parts.intersperse "/").foldl (· ++ ·) "" - let r := name.getRoot - let basic := if r == `Lean ∨ r == `Init ∨ r == `Std then - s!"https://github.com/leanprover/lean4/blob/{githash}/src/{path}.lean" + let root := module.getRoot + let basic := if root == `Lean ∨ root == `Init ∨ root == `Std then + s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean" else - s!"{baseUrl}/blob/{commit}/{path}.lean" + match ws.packageForModule? module with + | some pkg => + let (baseUrl, commit) := gitMap.find! pkg.name + s!"{baseUrl}/blob/{commit}/{path}.lean" + | none => "https://example.com" match range with | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}" | none => basic -def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do - let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker} +def htmlOutput (result : AnalyzerResult) (root : String) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do + let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash} let basePath := FilePath.mk "." / "build" / "doc" let indexHtml := ReaderT.run index config let findHtml := ReaderT.run find config diff --git a/Main.lean b/Main.lean index 4a7c71d..e8b2d82 100644 --- a/Main.lean +++ b/Main.lean @@ -7,12 +7,15 @@ open DocGen4 Lean Cli def runDocGenCmd (p : Parsed) : IO UInt32 := do let root := p.positionalArg! "root" |>.as! String let modules : List String := p.variableArgsAs! String |>.toList - let path ← lakeSetupSearchPath (←getLakePath) modules - IO.println s!"Loading modules from: {path}" - let doc ← load $ modules.map Name.mkSimple - IO.println "Outputting HTML" - htmlOutput doc root - pure 0 + let res ← lakeSetup modules + match res with + | Except.ok (ws, leanHash) => + IO.println s!"Loading modules from: {←searchPathRef.get}" + let doc ← load $ modules.map Name.mkSimple + IO.println "Outputting HTML" + htmlOutput doc root ws leanHash + pure 0 + | Except.error rc => pure rc def docGenCmd : Cmd := `[Cli| "doc-gen4" VIA runDocGenCmd; ["0.0.1"] diff --git a/lakefile.lean b/lakefile.lean index 9d9c138..d18d59c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -16,6 +16,10 @@ package «doc-gen4» { { name := `Cli src := Source.git "https://github.com/mhuisi/lean4-cli" "1f8663e3dafdcc11ff476d74ef9b99ae5bdaedd3" + }, + { + name := `lake + src := Source.git "https://github.com/leanprover/lake" "9378575b5575f49a185d50130743a190a9be2f82" } ] } From 0ec492ba98759f629c8e44c35fa8196489d3b977 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Mon, 14 Mar 2022 10:59:25 +0800 Subject: [PATCH 23/23] fix: error handling for declaration data --- static/declaration-data.js | 2 +- static/find/find.js | 38 ++++++++++++++++-------------- static/search.js | 48 ++++++++++++++++++++++++-------------- 3 files changed, 53 insertions(+), 35 deletions(-) diff --git a/static/declaration-data.js b/static/declaration-data.js index cb7a90c..2b778d5 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -56,7 +56,7 @@ export class DeclarationDataCenter { const timestamp = await timestampRes.text(); // try to use cache first - const data = await fetchCachedDeclarationData(timestamp); + const data = await fetchCachedDeclarationData(timestamp).catch(_e => null); if (data) { // if data is defined, use the cached one. DeclarationDataCenter.singleton = new DeclarationDataCenter(data); diff --git a/static/find/find.js b/static/find/find.js index 4b65f26..fbb9ca7 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -53,23 +53,27 @@ async function findAndRedirect(pattern, strict, view) { window.location.replace(`${SITE_ROOT}404.html`); } // search for result - const dataCenter = await DeclarationDataCenter.init(); - let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array - // if no result found, redirect to the 404 page - if (!result) { - // TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found. - window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`); - } else { - // success, redirect to doc or source page, or to the semantic rdf. - if (!view) { - window.location.replace(result.link); - } else if (view == "doc") { - window.location.replace(result.docLink); - } else if (view == "src") { - window.location.replace(result.sourceLink); + try { + const dataCenter = await DeclarationDataCenter.init(); + let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array + // if no result found, redirect to the 404 page + if (!result) { + // TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found. + window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`); } else { - // fallback to doc page - window.location.replace(result.docLink); + // success, redirect to doc or source page, or to the semantic rdf. + if (!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); + } } + } catch (e) { + document.write(`Cannot fetch data, please check your network connection.\n${e}`); } -} \ No newline at end of file +} diff --git a/static/search.js b/static/search.js index 1df8690..5b075de 100644 --- a/static/search.js +++ b/static/search.js @@ -4,7 +4,6 @@ import { DeclarationDataCenter } from "./declaration-data.js"; - const SEARCH_FORM = document.querySelector("#search_form"); const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]"); @@ -34,9 +33,7 @@ function handleSearchCursorUpDown(down) { * Perform search (when enter is pressed). */ function handleSearchEnter() { - const sel = - sr.querySelector(`.selected`) || - sr.firstChild; + const sel = sr.querySelector(`.selected`) || sr.firstChild; sel.click(); } @@ -72,9 +69,9 @@ function removeAllChildren(node) { } /** - * Search autocompletion. + * Handle user input and perform search. */ -SEARCH_INPUT.addEventListener("input", async (ev) => { +function handleSearch(dataCenter, err, ev) { const text = ev.target.value; // If no input clear all. @@ -86,19 +83,36 @@ SEARCH_INPUT.addEventListener("input", async (ev) => { // searching sr.setAttribute("state", "loading"); - const dataCenter = await DeclarationDataCenter.init(); - const result = dataCenter.search(text, false); - // in case user has updated the input. - if (ev.target.value != text) return; + if (dataCenter) { + const result = dataCenter.search(text, false); - // update search results - removeAllChildren(sr); - for (const { name, docLink } of result) { + // in case user has updated the input. + if (ev.target.value != text) return; + + // update search results + removeAllChildren(sr); + for (const { name, docLink } of result) { + const d = sr.appendChild(document.createElement("a")); + d.innerText = name; + d.title = name; + d.href = docLink; + } + } + // handle error + else { + removeAllChildren(sr); const d = sr.appendChild(document.createElement("a")); - d.innerText = name; - d.title = name; - d.href = docLink; + d.innerText = `Cannot fetch data, please check your network connection.\n${err}`; } sr.setAttribute("state", "done"); -}); +} + +DeclarationDataCenter.init() + .then((dataCenter) => { + // Search autocompletion. + SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev)); + }) + .catch(e => { + SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev)); + });