feat: add src endpoint

DocGen4/Output.lean

@@ -76,7 +76,8 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
       let name := decl.getName.toString
       let description := decl.getDocString.getD ""
       let link := Id.run <| ReaderT.run (declNameToLink decl.getName) config
-      let obj := Json.mkObj [("name", name), ("description", description), ("link", link)]
+      let source := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config
+      let obj := Json.mkObj [("name", name), ("description", description), ("link", link), ("source", source)]
       declList := declList.push obj
 
   let json := Json.arr declList

static/find/find.js

@@ -1,14 +1,22 @@
 import { SITE_ROOT } from "../site-root.js";
 import { declSearch } from "../search.js";
 
+async function findRedirect(query, isSource) {
+  return declSearch(query).then((results) => {
+    window.location.replace(isSource? results[0].source : results[0].link);
+  }).catch(() => {
+    window.location.replace(`${SITE_ROOT}404.html`);
+  });
+}
+
 let splits = window.location.href.split("#");
 
 if (splits.length < 2) {
   window.location.replace(`${SITE_ROOT}/404.html`);
 }
 
-declSearch(splits[1]).then((results) => {
-  window.location.replace(results[0].link);
-}).catch(() => {
-  window.location.replace(`${SITE_ROOT}404.html`);
-});
+if (splits[1].endsWith("/src")) {
+  findRedirect(splits[1].replace("/src", ""), true);
+} else {
+  findRedirect(splits[1], false);
+}

static/search.js

@@ -25,14 +25,14 @@ function matchCaseSensitive(declName, lowerDeclName, pat) {
 }
 
 export function loadDecls(searchableDataCnt) {
-    return searchableDataCnt.map(({name, description, link}) => [name, name.toLowerCase(), description.toLowerCase(), link]);
+    return searchableDataCnt.map(({name, description, link, source}) => [name, name.toLowerCase(), description.toLowerCase(), link, source]);
 }
 
 export function getMatches(decls, pat, maxResults = 30) {
     const lowerPats = pat.toLowerCase().split(/\s/g);
     const patNoSpaces = pat.replace(/\s/g, '');
     const results = [];
-    for (const [decl, lowerDecl, lowerDoc, link] of decls) {
+    for (const [decl, lowerDecl, lowerDoc, link, source] of decls) {
         let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces);
 
         // match all words as substrings of docstring
@@ -41,7 +41,7 @@ export function getMatches(decls, pat, maxResults = 30) {
         }
 
         if (err !== undefined) {
-            results.push({decl, err, link});
+            results.push({decl, err, link, source});
         }
     }
     return results.sort(({err: a}, {err: b}) => a - b).slice(0, maxResults);