feat: add jump-src.js for #src links

.gitignore

@@ -1,2 +1,3 @@
 /build
 /lake-packages/*
+lakefile.olean

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),

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"

DocGen4/Output/Template.lean

@@ -32,6 +32,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
 
         <script>{s!"const SITE_ROOT={String.quote (← getRoot)};"}</script>
         [moduleConstant]
+        <script type="module" src={s!"{← getRoot}jump-src.js"}></script>
         <script type="module" src={s!"{← getRoot}search.js"}></script>
         <script type="module" src={s!"{← getRoot}expand-nav.js"}></script>
         <script type="module" src={s!"{← getRoot}how-about.js"}></script>

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"

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",

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;
     }

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

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);
+  }
+})