diff --git a/.gitignore b/.gitignore
index 20c60d7..5bff016 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
/build
/lake-packages/*
+lakefile.olean
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 59ee753..8548b0f 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -42,6 +42,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
("declaration-data.js", declarationDataCenterJs),
("color-scheme.js", colorSchemeJs),
("nav.js", navJs),
+ ("jump-src.js", jumpSrcJs),
("expand-nav.js", expandNavJs),
("how-about.js", howAboutJs),
("search.html", searchHtml),
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 5c701ac..260bf47 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -149,6 +149,7 @@ are used in documentation generation, notably JS and CSS ones.
def styleCss : String := include_str "../../static/style.css"
def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
def colorSchemeJs : String := include_str "../../static/color-scheme.js"
+ def jumpSrcJs : String := include_str "../../static/jump-src.js"
def navJs : String := include_str "../../static/nav.js"
def expandNavJs : String := include_str "../../static/expand-nav.js"
def howAboutJs : String := include_str "../../static/how-about.js"
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index 979069c..5995e16 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -32,6 +32,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
[moduleConstant]
+
diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean
index 5b8dbb1..9502078 100644
--- a/DocGen4/Process/Hierarchy.lean
+++ b/DocGen4/Process/Hierarchy.lean
@@ -87,15 +87,16 @@ def baseDirBlackList : HashSet String :=
"color-scheme.js",
"declaration-data.js",
"declarations",
+ "expand-nav.js",
"find",
+ "foundational_types.html",
"how-about.js",
"index.html",
- "search.html",
- "foundational_types.html",
+ "jump-src.js",
"mathjax-config.js",
"navbar.html",
"nav.js",
- "expand-nav.js",
+ "search.html",
"search.js",
"src",
"style.css"
diff --git a/lakefile.lean b/lakefile.lean
index a609922..bc1d608 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -72,6 +72,7 @@ library_facet docs (lib) : FilePath := do
basePath / "declaration-data.js",
basePath / "color-scheme.js",
basePath / "nav.js",
+ basePath / "jump-src.js",
basePath / "expand-nav.js",
basePath / "how-about.js",
basePath / "search.js",
diff --git a/lakefile.olean b/lakefile.olean
deleted file mode 100644
index 6b2366a..0000000
Binary files a/lakefile.olean and /dev/null differ
diff --git a/static/declaration-data.js b/static/declaration-data.js
index 4c7352c..9884799 100644
--- a/static/declaration-data.js
+++ b/static/declaration-data.js
@@ -140,7 +140,7 @@ export class DeclarationDataCenter {
}
}
-function isSeparater(char) {
+function isSeparator(char) {
return char === "." || char === "_";
}
@@ -153,11 +153,11 @@ function matchCaseSensitive(declName, lowerDeclName, pattern) {
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);
+ err += (isSeparator(pattern[j]) ? 0.125 : 1) * (i - lastMatch);
if (pattern[j] !== declName[i]) err += 0.5;
lastMatch = i + 1;
j++;
- } else if (isSeparater(declName[i])) {
+ } else if (isSeparator(declName[i])) {
err += 0.125 * (i + 1 - lastMatch);
lastMatch = i + 1;
}
diff --git a/static/find/find.js b/static/find/find.js
index 5850a78..57953fc 100644
--- a/static/find/find.js
+++ b/static/find/find.js
@@ -80,6 +80,9 @@ async function findAndRedirect(pattern, strict, view) {
window.location.replace(result.link);
} else if (view == "doc") {
window.location.replace(result.docLink);
+ } else if (view == "src") {
+ const [module, decl] = result.docLink.split("#", 2);
+ window.location.replace(`${module}?jump=src#${decl}`);
} else {
// fallback to doc page
window.location.replace(result.docLink);
diff --git a/static/jump-src.js b/static/jump-src.js
new file mode 100644
index 0000000..e5c7371
--- /dev/null
+++ b/static/jump-src.js
@@ -0,0 +1,10 @@
+document.addEventListener("DOMContentLoaded", () => {
+ const hash = document.location.hash.substring(1);
+ const tgt = new URLSearchParams(document.location.search).get("jump");
+ if (tgt === "src" && hash) {
+ const target = document.getElementById(hash)
+ ?.querySelector(".gh_link a")
+ ?.getAttribute("href");
+ if (target) window.location.replace(target);
+ }
+})