From 06c20ee46f6a4dd32816725db885a1391cefb825 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 7 Apr 2022 12:39:32 +0200 Subject: [PATCH 1/3] dynamically change SITE_ROOT since we are relative now --- DocGen4/Output.lean | 2 -- DocGen4/Output/Base.lean | 1 - DocGen4/Output/Template.lean | 9 +++++---- static/declaration-data.js | 2 -- static/find/find.js | 1 - 5 files changed, 5 insertions(+), 10 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 5483cfe..f0d58bd 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -118,8 +118,6 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String FS.writeFile declarationDataPath json.compress 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 / "nav.js") navJs FS.writeFile (basePath / "find" / "find.js") findJs diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 2bae54a..60923d2 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -52,7 +52,6 @@ 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" diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 05390fe..c34051d 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -17,7 +17,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do {title} - + @@ -29,13 +29,14 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do - + + - + @@ -52,7 +53,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do [site] - + {←navbar} diff --git a/static/declaration-data.js b/static/declaration-data.js index 2b778d5..ad84854 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -4,8 +4,6 @@ * Please see {@link DeclarationDataCenter} for more information. */ -import { SITE_ROOT } from "./site-root.js"; - const CACHE_DB_NAME = "declaration-data"; const CACHE_DB_VERSION = 1; diff --git a/static/find/find.js b/static/find/find.js index fbb9ca7..00e25ed 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -15,7 +15,6 @@ * fallback to the `#doc` view. */ -import { SITE_ROOT } from "../site-root.js"; import { DeclarationDataCenter } from "../declaration-data.js"; /** From 67402506c7e37c32c6df4d7661fc025a29b9cbfb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 7 Apr 2022 12:44:33 +0200 Subject: [PATCH 2/3] fix: links in search --- DocGen4/Output.lean | 2 +- static/search.js | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index f0d58bd..ba53d21 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -94,7 +94,7 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String for (_, mod) in result.moduleInfo.toArray do for decl in filterMapDocInfo mod.members do let name := decl.getName.toString - let config := { config with depthToRoot := 2 } + let config := { config with depthToRoot := 0 } let doc := decl.getDocString.getD "" let root := Id.run <| ReaderT.run (getRoot) config let link := root ++ s!"../semantic/{decl.getName.hash}.xml#" diff --git a/static/search.js b/static/search.js index 5b075de..074d8bc 100644 --- a/static/search.js +++ b/static/search.js @@ -96,7 +96,7 @@ function handleSearch(dataCenter, err, ev) { const d = sr.appendChild(document.createElement("a")); d.innerText = name; d.title = name; - d.href = docLink; + d.href = SITE_ROOT + docLink; } } // handle error From 3ac6ddd1ab126a3c37c80088e4444dfe1532efb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 7 Apr 2022 13:14:01 +0200 Subject: [PATCH 3/3] fix: port the SITE_ROOT fix to find.js --- DocGen4/Output.lean | 2 +- DocGen4/Output/Find.lean | 1 + static/find/find.js | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index ba53d21..7919f67 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -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 basePath := FilePath.mk "." / "build" / "doc" 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 FS.createDirAll basePath FS.createDirAll (basePath / "find") diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean index 95bbd8e..e63507a 100644 --- a/DocGen4/Output/Find.lean +++ b/DocGen4/Output/Find.lean @@ -11,6 +11,7 @@ def find : HtmlM Html := do + diff --git a/static/find/find.js b/static/find/find.js index 00e25ed..8ce5b40 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -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. window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`); } else { + result.docLink = SITE_ROOT + result.docLink; // success, redirect to doc or source page, or to the semantic rdf. if (!view) { window.location.replace(result.link);