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] 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);