r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #48 from leanprover/fix-search 

Fix search
main
Henrik Böving 2022-04-07 13:20:31 +02:00 committed by GitHub
parent 00837fd089 3ac6ddd1ab
commit fa2f2b8e05
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 10 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
DocGen4/Output.lean
View File

@ -84,7 +84,7 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash} let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
let basePath := FilePath.mk "." / "build" / "doc" let basePath := FilePath.mk "." / "build" / "doc"
let indexHtml := ReaderT.run index config let indexHtml := ReaderT.run index config
let findHtml := ReaderT.run find config let findHtml := ReaderT.run find { config with depthToRoot := 1 }
let notFoundHtml := ReaderT.run notFound config let notFoundHtml := ReaderT.run notFound config
FS.createDirAll basePath FS.createDirAll basePath
FS.createDirAll (basePath / "find") FS.createDirAll (basePath / "find")
@ -94,7 +94,7 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
for (_, mod) in result.moduleInfo.toArray do for (_, mod) in result.moduleInfo.toArray do
for decl in filterMapDocInfo mod.members do for decl in filterMapDocInfo mod.members do
let name := decl.getName.toString let name := decl.getName.toString
let config := { config with depthToRoot := 2 } let config := { config with depthToRoot := 0 }
let doc := decl.getDocString.getD "" let doc := decl.getDocString.getD ""
let root := Id.run <| ReaderT.run (getRoot) config let root := Id.run <| ReaderT.run (getRoot) config
let link := root ++ s!"../semantic/{decl.getName.hash}.xml#" let link := root ++ s!"../semantic/{decl.getName.hash}.xml#"
@ -118,8 +118,6 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
FS.writeFile declarationDataPath json.compress FS.writeFile declarationDataPath json.compress
FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec
let root := Id.run <| ReaderT.run (getRoot) config
FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" root)
FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs
FS.writeFile (basePath / "nav.js") navJs FS.writeFile (basePath / "nav.js") navJs
FS.writeFile (basePath / "find" / "find.js") findJs FS.writeFile (basePath / "find" / "find.js") findJs

1
DocGen4/Output/Base.lean
View File

@ -52,7 +52,6 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
section Static section Static
def styleCss : String := include_str "../../static/style.css" 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 declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
def navJs : String := include_str "../../static/nav.js" def navJs : String := include_str "../../static/nav.js"
def howAboutJs : String := include_str "../../static/how-about.js" def howAboutJs : String := include_str "../../static/how-about.js"

1
DocGen4/Output/Find.lean
View File

@ -11,6 +11,7 @@ def find : HtmlM Html := do
<html lang="en"> <html lang="en">
<head> <head>
<link rel="preload" href={s!"{←getRoot}declaration-data.bmp"}/> <link rel="preload" href={s!"{←getRoot}declaration-data.bmp"}/>
<script>{s!"const SITE_ROOT={String.quote (←getRoot)};"}</script>
<script type="module" async="true" src={s!"./find.js"}></script> <script type="module" async="true" src={s!"./find.js"}></script>
</head> </head>
<body></body> <body></body>

1
DocGen4/Output/Template.lean
View File

@ -30,6 +30,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
<script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script> <script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
<script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script> <script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
<script>{s!"const SITE_ROOT={String.quote (←getRoot)};"}</script>
<script type="module" src={s!"{←getRoot}nav.js"}></script> <script type="module" src={s!"{←getRoot}nav.js"}></script>
<script type="module" src={s!"{←getRoot}search.js"}></script> <script type="module" src={s!"{←getRoot}search.js"}></script>
<script type="module" src={s!"{←getRoot}how-about.js"}></script> <script type="module" src={s!"{←getRoot}how-about.js"}></script>

2
static/declaration-data.js
View File

@ -4,8 +4,6 @@
* Please see {@link DeclarationDataCenter} for more information. * Please see {@link DeclarationDataCenter} for more information.
*/ */
import { SITE_ROOT } from "./site-root.js";
const CACHE_DB_NAME = "declaration-data"; const CACHE_DB_NAME = "declaration-data";
const CACHE_DB_VERSION = 1; const CACHE_DB_VERSION = 1;

2
static/find/find.js
View File

@ -15,7 +15,6 @@
* fallback to the `#doc` view. * fallback to the `#doc` view.
*/ */
import { SITE_ROOT } from "../site-root.js";
import { DeclarationDataCenter } from "../declaration-data.js"; import { DeclarationDataCenter } from "../declaration-data.js";
/** /**
@ -61,6 +60,7 @@ async function findAndRedirect(pattern, strict, view) {
// TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found. // 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 ?? ""}`); window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`);
} else { } else {
result.docLink = SITE_ROOT + result.docLink;
// success, redirect to doc or source page, or to the semantic rdf. // success, redirect to doc or source page, or to the semantic rdf.
if (!view) { if (!view) {
window.location.replace(result.link); window.location.replace(result.link);

2
static/search.js
View File

@ -96,7 +96,7 @@ function handleSearch(dataCenter, err, ev) {
const d = sr.appendChild(document.createElement("a")); const d = sr.appendChild(document.createElement("a"));
d.innerText = name; d.innerText = name;
d.title = name; d.title = name;
d.href = docLink; d.href = SITE_ROOT + docLink;
} }
} }
// handle error // handle error