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

fix: port the SITE_ROOT fix to find.js

main
Henrik Böving 2022-04-07 13:14:01 +02:00
parent 67402506c7
commit 3ac6ddd1ab
3 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
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")

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
static/find/find.js
View File

@ -60,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);