URLs now work; Data fetching does not?

DocGen4/IncludeStr.lean

@@ -7,13 +7,37 @@ import Lean
 
 namespace DocGen4
 
-open Lean System IO Lean.Elab.Term
+open Lean System IO Lean.Elab.Term FS
+
+deriving instance DecidableEq for FileType
+
+/--
+  Traverse all subdirectories fo `f` to find if one satisfies `p`.
+-/
+partial def traverseDir (f : FilePath) (p : FilePath → IO Bool) : IO (Option FilePath) := do
+  if (← p f) then
+    return f
+  for d in (← System.FilePath.readDir f) do
+    let subDir := d.path
+    let metadata ← subDir.metadata
+    if metadata.type = FileType.dir then
+      if let some p ← traverseDir subDir p then
+        return p
+  return none
 
 syntax (name := includeStr) "include_str" str : term
 
 @[termElab includeStr] def includeStrImpl : TermElab := λ stx expectedType? => do
-    let str := stx[1].isStrLit?.get!
+  let str := stx[1].isStrLit?.get!
-    let path := FilePath.mk str
+  let srcPath := (FilePath.mk (← read).fileName)
+  let currentDir ← IO.currentDir
+  -- HACK: Currently we cannot get current file path in VSCode, we have to traversely find the matched subdirectory in the current directory.
+  if let some path ← match srcPath.parent with
+  | some p => pure $ some $ p / str
+  | none => do
+    let foundDir ← traverseDir currentDir λ p => p / str |>.pathExists 
+    pure $ foundDir.map (· / str)
+  then 
     if ←path.pathExists then
       if ←path.isDir then
         throwError s!"{str} is a directory"
@@ -21,6 +45,8 @@ syntax (name := includeStr) "include_str" str : term
         let content ← FS.readFile path
         pure $ mkStrLit content
     else
-      throwError s!"\"{str}\" does not exist as a file"
+      throwError s!"{path} does not exist as a file"
+  else
+    throwError s!"No such file in whole directory: {str}"
 
 end DocGen4

DocGen4/Load.lean

@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 
 import Lean
+import Lake
 import DocGen4.Process
 import Std.Data.HashMap
 
@@ -12,40 +13,25 @@ namespace DocGen4
 
 open Lean System Std IO
 
-def getLakePath : IO FilePath := do
+def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do
-  match (← IO.getEnv "LAKE") with
+  let (leanInstall?, lakeInstall?) ← Lake.findInstall?
-  | some path => pure $ System.FilePath.mk path
+  let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO'
-  | none =>
+  match res with
-    let lakePath := (←findSysroot?) / "bin" / "lake"
+  | Except.ok (ws, options) =>
-    pure $ lakePath.withExtension System.FilePath.exeExtension
+    let lean := leanInstall?.get!
-
+    if lean.githash ≠ Lean.githash then
--- Modified from the LSP Server
+      IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {lean.githash}"
-def lakeSetupSearchPath (lakePath : System.FilePath) (imports : Array String) : IO Lean.SearchPath := do
+    let lake := lakeInstall?.get!
-  let args := #["print-paths"] ++ imports
+    let ctx ← Lake.mkBuildContext ws lean lake
-  let cmdStr := " ".intercalate (toString lakePath :: args.toList)
+    ws.root.buildImportsAndDeps imports |>.run Lake.LogMethods.eio ctx
-  let lakeProc ← Process.spawn {
+    initSearchPath (←findSysroot) ws.leanPaths.oleanPath
-    stdin  := Process.Stdio.null
+    pure $ Except.ok (ws, lean.githash)
-    stdout := Process.Stdio.piped
+  | Except.error rc => pure $ Except.error rc
-    stderr := Process.Stdio.piped
-    cmd    := lakePath.toString
-    args
-  }
-  let stdout := String.trim (← lakeProc.stdout.readToEnd)
-  let stderr := String.trim (← lakeProc.stderr.readToEnd)
-  match (← lakeProc.wait) with
-  | 0 =>
-    let stdout := stdout.split (· == '\n') |>.getLast!
-    let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?)
-      | throw $ userError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}"
-    initSearchPath (← findSysroot?) paths.oleanPath
-    paths.oleanPath.mapM realPathNormalized
-  | 2 => pure []  -- no lakefile.lean
-  | _ => throw $ userError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}"
 
 def load (imports : List Name) : IO AnalyzerResult := do
   let env ← importModules (List.map (Import.mk · false) imports) Options.empty
   -- TODO parameterize maxHeartbeats
   IO.println "Processing modules"
-  Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {})
+  Prod.fst <$> Meta.MetaM.toIO process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
 
 end DocGen4

DocGen4/Output.lean

@@ -4,12 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 import Lean
+import Lake
 import DocGen4.Process
 import DocGen4.Output.Base
 import DocGen4.Output.Index
 import DocGen4.Output.Module
 import DocGen4.Output.NotFound
 import DocGen4.Output.Find
+import DocGen4.Output.Semantic
 
 namespace DocGen4
 
@@ -24,12 +26,8 @@ Three link types from git supported:
 TODO: This function is quite brittle and very github specific, we can
 probably do better.
 -/
-def getGithubBaseUrl : IO String := do
+def getGithubBaseUrl (gitUrl : String) : String := Id.run do
-  let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
+  let mut url := gitUrl
-  if out.exitCode != 0 then
-    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
-  let mut url := out.stdout.trimRight
-
   if url.startsWith "git@" then
     url := url.drop 15
     url := url.dropRight 4
@@ -39,57 +37,106 @@ def getGithubBaseUrl : IO String := do
   else
     pure url
 
-def getCommit : IO String := do
+def getProjectGithubUrl : IO String := do
+  let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
+  if out.exitCode != 0 then
+    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
+  pure out.stdout.trimRight
+
+def getProjectCommit : IO String := do
   let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]}
   if out.exitCode != 0 then
     throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
   pure out.stdout.trimRight
 
-def sourceLinker : IO (Name → Option DeclarationRange → String) := do
+def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do
-  let baseUrl ← getGithubBaseUrl
+  -- Compute a map from package names to source URL
-  let commit ← getCommit
+  let mut gitMap := Std.mkHashMap
-  pure λ name range =>
+  let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
-    let parts := name.components.map Name.toString
+  let projectCommit ← getProjectCommit
+  gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
+  for pkg in ws.packageArray do
+    for dep in pkg.dependencies do
+      let value := match dep.src with
+        | Lake.Source.git url commit => (getGithubBaseUrl url, commit)
+        -- TODO: What do we do here if linking a source is not possible?
+        | _ => ("https://example.com", "master")
+      gitMap := gitMap.insert dep.name value
+
+  pure $ λ module range =>
+    let parts := module.components.map Name.toString
     let path := (parts.intersperse "/").foldl (· ++ ·) ""
-    let r := name.getRoot
+    let root := module.getRoot
-    let basic := if r == `Lean ∨ r == `Init ∨ r == `Std then
+    let basic := if root == `Lean ∨ root == `Init ∨ root == `Std then
-      s!"https://github.com/leanprover/lean4/blob/{githash}/src/{path}.lean"
+      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
     else
-      s!"{baseUrl}/blob/{commit}/{path}.lean"
+      match ws.packageForModule? module with
+      | some pkg =>
+        let (baseUrl, commit) := gitMap.find! pkg.name
+        s!"{baseUrl}/blob/{commit}/{path}.lean"
+      | none => "https://example.com"
 
     match range with
     | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
     | none => basic
 
-def htmlOutput (result : AnalyzerResult) : IO Unit := do
+def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
-  let basePath := FilePath.mk "./build/doc/"
+  let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
-  let config := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker}
+  let basePath := FilePath.mk "." / "build" / "doc"
+  let indexHtml := ReaderT.run index config 
+  let findHtml := ReaderT.run find config
+  let notFoundHtml := ReaderT.run notFound config
   FS.createDirAll basePath
   FS.createDirAll (basePath / "find")
-  let indexHtml := ReaderT.run index config 
+  FS.createDirAll (basePath / "semantic")
-  let notFoundHtml := ReaderT.run notFound config
 
   let mut declList := #[]
   for (module, mod) in result.moduleInfo.toArray do
     for decl in filterMapDocInfo mod.members do
-      let findDir := basePath / "find" / decl.getName.toString
+-- <<<<<<< HEAD
-      let findFile := (findDir / "index.html")
+      let name := decl.getName.toString
-      -- path: 'basePath/find/decl.getName.toString'
+      -- let findDir := basePath / "find" / ma,e
+      -- let findFile := (findDir / "index.html")
       let config := { config with depthToRoot := 2 }
-      let findHtml := ReaderT.run (findRedirectHtml decl.getName) config
+      -- let findHtml := ReaderT.run (findRedirectHtml decl.getName) config
-      FS.createDirAll findDir
+      -- FS.createDirAll findDir
-      FS.writeFile findFile findHtml.toString
+      -- FS.writeFile findFile findHtml.toString
-      let obj := Json.mkObj [("name", decl.getName.toString), ("description", decl.getDocString.getD "")]
+      -- let obj := Json.mkObj [("name", decl.getName.toString), ("description", decl.getDocString.getD "")]
+-- =======
+      let doc := decl.getDocString.getD ""
+      -- let root := module.getRoot 
+      let root := Id.run <| ReaderT.run (getRoot) config
+      let link :=  root ++ s!"../semantic/{decl.getName.hash}.xml#"
+      let docLink := Id.run <| ReaderT.run (declNameToLink decl.getName) config
+      let sourceLink := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config
+      let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourceLink", sourceLink)]
+-- >>>>>>> upstream/main
       declList := declList.push obj
+      let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config 
+      FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml
   let json := Json.arr declList
 
-  FS.writeFile (basePath / "searchable_data.bmp") json.compress
+  FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config 
+
   FS.writeFile (basePath / "index.html") indexHtml.toString
-  FS.writeFile (basePath / "style.css") styleCss
   FS.writeFile (basePath / "404.html") notFoundHtml.toString
+  FS.writeFile (basePath / "find" / "index.html") findHtml.toString
+
+  FS.writeFile (basePath / "style.css") styleCss
+
+  let declarationDataPath := basePath / "declaration-data.bmp"
+  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
+  FS.writeFile (basePath / "how-about.js") howAboutJs
   FS.writeFile (basePath / "search.js") searchJs
   FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs
+
   for (module, content) in result.moduleInfo.toArray do
     let fileDir := moduleNameToDirectory basePath module
     let filePath := moduleNameToFile basePath module

DocGen4/Output/Base.lean

@@ -53,10 +53,14 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
   basePath / parts.foldl (· / ·) (FilePath.mk ".")
 
 section Static
-  def styleCss : String := include_str "./static/style.css"
+  def styleCss : String := include_str "../../static/style.css"
-  def navJs : String := include_str "./static/nav.js"
+  def siteRootJs : String := include_str "../../static/site-root.js"
-  def searchJs : String := include_str "./static/search.js"
+  def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
-  def mathjaxConfigJs : String := include_str "./static/mathjax-config.js"
+  def navJs : String := include_str "../../static/nav.js"
+  def howAboutJs : String := include_str "../../static/how-about.js"
+  def searchJs : String := include_str "../../static/search.js"
+  def findJs : String := include_str "../../static/find/find.js"
+  def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
 end Static
 
 def declNameToLink (name : Name) : HtmlM String := do

DocGen4/Output/Find.lean

@@ -6,10 +6,16 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean
 
-def findRedirectHtml (decl : Name) : HtmlM Html := do
+def find : HtmlM Html := do
-  let res ← getResult
+  pure
-  let url ← declNameToLink decl
+    <html lang="en">
-  let contentString := s!"0;url={url}"
+      <head>
-  pure $ Html.element "meta" false #[("http-equiv", "refresh"), ("content", contentString)] #[]
+        <link rel="preload" href={s!"{←getRoot}declaration-data.bmp"}/>
+        <script type="module" async="true" src={s!"./find.js"}></script>
+      </head>
+      <body></body>
+    </html>
+
 end Output
 end DocGen4
+

DocGen4/Output/Navbar.lean

@@ -14,7 +14,7 @@ open Lean
 open scoped DocGen4.Jsx
 
 def moduleListFile (file : Name) : HtmlM Html := do
-  pure <div "class"="nav_link" [if (← getCurrentName) == file then #[("visible", "")] else #[]]>
+  pure <div «class»={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
     <a href={← moduleNameToLink file}>{file.toString}</a>
   </div>
 
@@ -29,7 +29,12 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   pure
     <details "class"="nav_sect" "data-path"={moduleLink}
       [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
-      {Html.element "summary" true #[] #[<a "href"={← moduleNameToLink h.getName}>{h.getName.toString}</a>]}
+      {
+        if (←getResult).moduleInfo.contains h.getName then
+          Html.element "summary" true #[] #[<a "href"={← moduleNameToLink h.getName}>{h.getName.toString}</a>]
+        else
+          <summary>{h.getName.toString}</summary>
+      }
       [dirNodes]
       [fileNodes]
     </details>

DocGen4/Output/Semantic.lean

@@ -0,0 +1,58 @@
+import DocGen4.Output.Template
+import DocGen4.Output.DocString
+import Lean.Data.Xml
+
+open Lean Xml
+
+namespace DocGen4
+namespace Output
+
+instance : ToString $ Array Element where
+  toString xs := xs.map toString |>.foldl String.append ""
+
+instance : Coe Element Content where
+  coe e := Content.Element e
+
+-- TODO: syntax metaprogramming and basic semantic data
+
+def semanticXml (i : DocInfo) : HtmlM $ Array Element := do
+  pure #[
+    Element.Element
+      "rdf:RDF"
+        (Std.RBMap.fromList [
+          ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"),
+          ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#")
+        ] _)
+        #[
+          Element.Element
+          "rdf:Description" 
+          (Std.RBMap.fromList [
+            ("rdf:about", s!"{←getRoot}semactic/{i.getName.hash}.xml#")
+          ] _)
+         #[]
+        ]
+  ]
+
+def schemaXml : HtmlM $ Array Element := do
+  pure #[
+    Element.Element
+      "rdf:RDF"
+        (Std.RBMap.fromList [
+          ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"),
+          ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#")
+        ] _)
+        #[
+          Element.Element
+          "docgen4:hasInstance" 
+          Std.RBMap.empty
+          #[
+            Element.Element
+            "rdfs:type" 
+            Std.RBMap.empty
+            #[Content.Character "rdf:Property"]
+          ]
+        ]
+  ]
+
+end Output
+end DocGen4

DocGen4/Output/Template.lean

@@ -15,46 +15,48 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
   pure
     <html lang="en">
       <head>
+
+        <title>{title}</title>
+        
+        <meta charset="UTF-8"/>
+        <meta name="viewport" content="width=device-width, initial-scale=1"/>
+
         <link rel="stylesheet" href={s!"{←getRoot}style.css"}/>
         <link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>
         <link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
-        <title>{title}</title>
+        <link rel="prefetch" href={s!"{←getRoot}declaration-data.bmp"}/>
-        <meta charset="UTF-8"/>
+
-        <meta name="viewport" content="width=device-width, initial-scale=1"/>
+        <script defer="true" src={s!"{←getRoot}mathjax-config.js"}></script>
+        <script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
+        <script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
+        
+        <script type="module" src={s!"{←getRoot}nav.js"}></script>
+        <script type="module" src={s!"{←getRoot}search.js"}></script>
+        <script type="module" src={s!"{←getRoot}how-about.js"}></script>
+
       </head>
       
       <body>
 
-      <input id="nav_toggle" type="checkbox"/>
+        <input id="nav_toggle" type="checkbox"/>
 
-      <header>
+        <header>
-        <h1><label «for»="nav_toggle"></label>Documentation</h1>
+          <h1><label «for»="nav_toggle"></label>Documentation</h1>
-        <p «class»="header_filename break_within">{title}</p>
+          <p «class»="header_filename break_within">{title}</p>
-        -- TODO: Replace this form with our own search
+          -- TODO: Replace this form with our own search
-        <form action="https://google.com/search" method="get" id="search_form">
+          <form action="https://google.com/search" method="get" id="search_form">
-          <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib_docs"/>
+            <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib_docs"/>
-          <input type="text" name="q" autocomplete="off"/>
+            <input type="text" name="q" autocomplete="off"/>
-          <button>Google site search</button>
+            <button>Google site search</button>
-        </form>
+          </form>
-      </header>
+        </header>
 
-      [site]
+        [site]
-      
+        
-      {←navbar}
+        {←navbar}
 
-      -- Lean in JS in HTML in Lean...very meta
-      <script>
-        siteRoot = "{←getRoot}";
-      </script>
-
-      -- TODO Add more js stuff
-      <script src={s!"{←getRoot}nav.js"}></script>
-      <script src={s!"{←getRoot}search.js"}></script>
-      -- mathjax
-      <script src={s!"{←getRoot}mathjax-config.js"}></script>
-      <script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
-      <script src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
       </body>
+
     </html>
 
 

Main.lean

@@ -1,15 +1,30 @@
 import DocGen4
 import Lean
+import Cli
 
-open DocGen4 Lean IO
+open DocGen4 Lean Cli
 
-def main (modules : List String) : IO Unit := do
+def runDocGenCmd (p : Parsed) : IO UInt32 := do
-  if modules.isEmpty then
+  -- let root := p.positionalArg! "root" |>.as! String
-    IO.println "Usage: doc-gen4 Module1 Module2 ..."
+  let modules : List String := p.variableArgsAs! String |>.toList
-    IO.Process.exit 1
+  let res ← lakeSetup modules
-    return
+  match res with
-  let path ← lakeSetupSearchPath (←getLakePath) modules.toArray
+  | Except.ok (ws, leanHash) =>
-  IO.println s!"Loading modules from: {path}"
+    IO.println s!"Loading modules from: {←searchPathRef.get}"
-  let doc ← load $ modules.map Name.mkSimple
+    let doc ← load $ modules.map Name.mkSimple
-  IO.println "Outputting HTML"
+    IO.println "Outputting HTML"
-  htmlOutput doc
+    htmlOutput doc ws leanHash
+    pure 0
+  | Except.error rc => pure rc
+
+def docGenCmd : Cmd := `[Cli|
+  "doc-gen4" VIA runDocGenCmd; ["0.0.1"]
+  "A documentation generator for Lean 4."
+
+  ARGS:
+    -- root : String; "The root URL to generate the HTML for (will be relative in the future)"
+    ...modules : String; "The modules to generate the HTML for"
+]
+
+def main (args : List String) : IO UInt32 :=
+  docGenCmd.validate args

lakefile.lean

@@ -12,6 +12,14 @@ package «doc-gen4» {
     {
       name := `Unicode
       src := Source.git "https://github.com/xubaiw/Unicode.lean" "3b7b85472d42854a474099928a3423bb97d4fa64"
+    },
+    {
+      name := `Cli
+      src := Source.git "https://github.com/mhuisi/lean4-cli" "1f8663e3dafdcc11ff476d74ef9b99ae5bdaedd3"
+    },
+    {
+      name := `lake
+      src := Source.git "https://github.com/leanprover/lake" "9378575b5575f49a185d50130743a190a9be2f82"
     }
   ]
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-17
+leanprover/lean4:nightly-2022-03-06

static/declaration-data.js

@@ -0,0 +1,243 @@
+/**
+ * This module is a wrapper that facilitates manipulating the declaration data.
+ *
+ * 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;
+
+/**
+ * The DeclarationDataCenter is used for declaration searching.
+ *
+ * For usage, see the {@link init} and {@link search} methods.
+ */
+export class DeclarationDataCenter {
+  /**
+   * The declaration data. Users should not interact directly with this field.
+   *
+   * *NOTE:* This is not made private to support legacy browsers.
+   */
+  declarationData = null;
+
+  /**
+   * Used to implement the singleton, in case we need to fetch data mutiple times in the same page.
+   */
+  static singleton = null;
+
+  /**
+   * Construct a DeclarationDataCenter with given data.
+   *
+   * Please use {@link DeclarationDataCenter.init} instead, which automates the data fetching process.
+   * @param {*} declarationData
+   */
+  constructor(declarationData) {
+    this.declarationData = declarationData;
+  }
+
+  /**
+   * The actual constructor of DeclarationDataCenter
+   * @returns {Promise<DeclarationDataCenter>}
+   */
+  static async init() {
+    if (!DeclarationDataCenter.singleton) {
+      const timestampUrl = new URL(
+        `${SITE_ROOT}declaration-data.timestamp`,
+        window.location
+      );
+      const dataUrl = new URL(
+        `${SITE_ROOT}declaration-data.bmp`,
+        window.location
+      );
+
+      const timestampRes = await fetch(timestampUrl);
+      const timestamp = await timestampRes.text();
+
+      // try to use cache first
+      const data = await fetchCachedDeclarationData(timestamp).catch(_e => null);
+      if (data) {
+        // if data is defined, use the cached one.
+        DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
+      } else {
+        // undefined. then fetch the data from the server.
+        const dataRes = await fetch(dataUrl);
+        const dataJson = await dataRes.json();
+        // the data is a map of name (original case) to declaration data.
+        const data = new Map(
+          dataJson.map(({ name, doc, link, docLink, sourceLink }) => [
+            name,
+            {
+              name,
+              lowerName: name.toLowerCase(),
+              lowerDoc: doc.toLowerCase(),
+              link,
+              docLink,
+              sourceLink,
+            },
+          ])
+        );
+        await cacheDeclarationData(timestamp, data);
+        DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
+      }
+    }
+    return DeclarationDataCenter.singleton;
+  }
+
+  /**
+   * Search for a declaration.
+   * @returns {Array<any>}
+   */
+  search(pattern, strict = true) {
+    if (!pattern) {
+      return [];
+    }
+    if (strict) {
+      let decl = this.declarationData.get(pattern);
+      return decl ? [decl] : [];
+    } else {
+      return getMatches(this.declarationData, pattern);
+    }
+  }
+}
+
+function isSeparater(char) {
+  return char === "." || char === "_";
+}
+
+// HACK: the fuzzy matching is quite hacky
+
+function matchCaseSensitive(declName, lowerDeclName, pattern) {
+  let i = 0,
+    j = 0,
+    err = 0,
+    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);
+      if (pattern[j] !== declName[i]) err += 0.5;
+      lastMatch = i + 1;
+      j++;
+    } else if (isSeparater(declName[i])) {
+      err += 0.125 * (i + 1 - lastMatch);
+      lastMatch = i + 1;
+    }
+    i++;
+  }
+  err += 0.125 * (declName.length - lastMatch);
+  if (j === pattern.length) {
+    return err;
+  }
+}
+
+function getMatches(declarations, pattern, maxResults = 30) {
+  const lowerPats = pattern.toLowerCase().split(/\s/g);
+  const patNoSpaces = pattern.replace(/\s/g, "");
+  const results = [];
+  for (const {
+    name,
+    lowerName,
+    lowerDoc,
+    link,
+    docLink,
+    sourceLink,
+  } of declarations.values()) {
+    let err = matchCaseSensitive(name, lowerName, patNoSpaces);
+    // match all words as substrings of docstring
+    if (
+      err >= 3 &&
+      pattern.length > 3 &&
+      lowerPats.every((l) => lowerDoc.indexOf(l) != -1)
+    ) {
+      err = 3;
+    }
+    if (err !== undefined) {
+      results.push({
+        name,
+        err,
+        lowerName,
+        lowerDoc,
+        link,
+        docLink,
+        sourceLink,
+      });
+    }
+  }
+  return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults);
+}
+
+// TODO: refactor the indexedDB part to be more robust
+
+/**
+ * Get the indexedDB database, automatically initialized.
+ * @returns {Promise<IDBDatabase>}
+ */
+async function getDeclarationDatabase() {
+  return new Promise((resolve, reject) => {
+    const request = indexedDB.open(CACHE_DB_NAME, CACHE_DB_VERSION);
+
+    request.onerror = function (event) {
+      reject(
+        new Error(
+          `fail to open indexedDB ${CACHE_DB_NAME} of version ${CACHE_DB_VERSION}`
+        )
+      );
+    };
+    request.onupgradeneeded = function (event) {
+      let db = event.target.result;
+      // We only need to store one object, so no key path or increment is needed.
+      db.createObjectStore("declaration");
+    };
+    request.onsuccess = function (event) {
+      resolve(event.target.result);
+    };
+  });
+}
+
+/**
+ * Store data in indexedDB object store.
+ * @param {string} timestamp
+ * @param {Map<string, any>} data
+ */
+async function cacheDeclarationData(timestamp, data) {
+  let db = await getDeclarationDatabase();
+  let store = db
+    .transaction("declaration", "readwrite")
+    .objectStore("declaration");
+  return new Promise((resolve, reject) => {
+    let clearRequest = store.clear();
+    let addRequest = store.add(data, timestamp);
+
+    addRequest.onsuccess = function (event) {
+      resolve();
+    };
+    addRequest.onerror = function (event) {
+      reject(new Error(`fail to store declaration data`));
+    };
+    clearRequest.onerror = function (event) {
+      reject(new Error("fail to clear object store"));
+    };
+  });
+}
+
+/**
+ * Retrieve data from indexedDB database.
+ * @param {string} timestamp
+ * @returns {Promise<Map<string, any>|undefined>}
+ */
+async function fetchCachedDeclarationData(timestamp) {
+  let db = await getDeclarationDatabase();
+  let store = db
+    .transaction("declaration", "readonly")
+    .objectStore("declaration");
+  return new Promise((resolve, reject) => {
+    let transactionRequest = store.get(timestamp);
+    transactionRequest.onsuccess = function (event) {
+      resolve(event.result);
+    };
+    transactionRequest.onerror = function (event) {
+      reject(new Error(`fail to store declaration data`));
+    };
+  });
+}

static/find/find.js

@@ -0,0 +1,79 @@
+/**
+ * This module is used for the `/find` endpoint.
+ *
+ * Two basic kinds of search syntax are supported:
+ *
+ * 1. Query-Fragment syntax: `/find?pattern=Nat.add#doc` for documentation and `/find?pattern=Nat.add#src` for source code.
+ * 2. Fragment-Only syntax:`/find/#doc/Nat.add` for documentation and `/find/#src/Nat.add` for source code.
+ *
+ * Though both of them are valid, the first one is highly recommended, and the second one is for compatibility and taste.
+ *
+ * There are some extended usage for the QF syntax. For example, appending `strict=false` to the query part
+ * (`/find?pattern=Nat.add&strict=false#doc`) will allow you to use the fuzzy search, rather than strict match.
+ * Also, the fragment is extensible as well. For now only `#doc` and `#src` are implement, and the plain query without
+ * hash (`/find?pattern=Nat.add`) is used for computer-friendly data (semantic web is great! :P), while all other fragments
+ * fallback to the `#doc` view.
+ */
+
+import { SITE_ROOT } from "../site-root.js";
+import { DeclarationDataCenter } from "../declaration-data.js";
+
+/**
+ * We don't use browser's default hash and searchParams in case Lean declaration name
+ * can be like `«#»`, rather we manually handle the `window.location.href` with regex.
+ */
+const LEAN_FRIENDLY_URL_REGEX = /^[^?#]+(?:\?((?:[^«#»]|«.*»)*))?(?:#(.*))?$/;
+const LEAN_FRIENDLY_AND_SEPARATOR = /(?<!«[^»]*)&/;
+const LEAN_FRIENDLY_EQUAL_SEPARATOR = /(?<!«[^»]*)=/;
+const LEAN_FRIENDLY_SLASH_SEPARATOR = /(?<!«[^»]*)\//;
+
+const [_, query, fragment] = LEAN_FRIENDLY_URL_REGEX.exec(window.location.href);
+const queryParams = new Map(
+  query
+    ?.split(LEAN_FRIENDLY_AND_SEPARATOR)
+    ?.map((p) => p.split(LEAN_FRIENDLY_EQUAL_SEPARATOR))
+    ?.filter((l) => l.length == 2 && l[0].length > 0)
+);
+const fragmentPaths = fragment?.split(LEAN_FRIENDLY_SLASH_SEPARATOR) ?? [];
+
+const pattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail then second, may be undefined
+const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true
+const view = fragmentPaths[0];
+
+findAndRedirect(pattern, strict, view);
+
+/**
+ * Find the result and redirect to the result page.
+ * @param {string} pattern the pattern to search for
+ * @param {string} view the view of the find result (`"doc"` or `"src"` for now)
+ */
+async function findAndRedirect(pattern, strict, view) {
+  // if no pattern provided, directly redirect to the 404 page
+  if (!pattern) {
+    window.location.replace(`${SITE_ROOT}404.html`);
+  }
+  // search for result
+  try {
+    const dataCenter = await DeclarationDataCenter.init();
+    let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array
+    // if no result found, redirect to the 404 page
+    if (!result) {
+      // 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 {
+      // success, redirect to doc or source page, or to the semantic rdf.
+      if (!view) {
+        window.location.replace(result.link);
+      } else if (view == "doc") {
+        window.location.replace(result.docLink);
+      } else if (view == "src") {
+        window.location.replace(result.sourceLink);
+      } else {
+        // fallback to doc page
+        window.location.replace(result.docLink);
+      }
+    }
+  } catch (e) {
+    document.write(`Cannot fetch data, please check your network connection.\n${e}`);
+  }
+}

static/how-about.js

@@ -0,0 +1,39 @@
+/**
+ * This module implements the `howabout` functionality in the 404 page.
+ */
+
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+const HOW_ABOUT = document.querySelector("#howabout");
+
+// Show url of the missing page
+if (HOW_ABOUT) {
+  HOW_ABOUT.parentNode
+    .insertBefore(document.createElement("pre"), HOW_ABOUT)
+    .appendChild(document.createElement("code")).innerText =
+    window.location.href.replace(/[/]/g, "/\u200b");
+
+  // TODO: add how about functionality for similar page as well.
+  const pattern = window.location.hash.replace("#", "");
+
+  // try to search for similar declarations
+  if (pattern) {
+    HOW_ABOUT.innerText = "Please wait a second. I'll try to help you.";
+    DeclarationDataCenter.init().then((dataCenter) => {
+      let results = dataCenter.search(pattern, false);
+      if (results.length > 0) {
+        HOW_ABOUT.innerText = "How about one of these instead:";
+        const ul = HOW_ABOUT.appendChild(document.createElement("ul"));
+        for (const { name, docLink } of results) {
+          const li = ul.appendChild(document.createElement("li"));
+          const a = li.appendChild(document.createElement("a"));
+          a.href = docLink;
+          a.appendChild(document.createElement("code")).innerText = name;
+        }
+      } else {
+        HOW_ABOUT.innerText =
+          "Sorry, I cannot find any similar declarations. Check the link or use the module navigation to find what you want :P";
+      }
+    });
+  }
+}

static/mathjax-config.js

@@ -1,17 +1,41 @@
+/*
+ * This file is for configing MathJax behavior.
+ * See https://docs.mathjax.org/en/latest/web/configuration.html
+ * 
+ * This configuration is copied from old doc-gen3
+ * https://github.com/leanprover-community/doc-gen
+ */
 MathJax = {
-    tex: {
+  tex: {
-        inlineMath: [['$', '$']],
+    inlineMath: [["$", "$"]],
-        displayMath: [['$$', '$$']]
+    displayMath: [["$$", "$$"]],
-    },
+  },
-    options: {
+  options: {
-        skipHtmlTags: [
+    skipHtmlTags: [
-            'script', 'noscript', 'style', 'textarea', 'pre',
+      "script",
-            'code', 'annotation', 'annotation-xml',
+      "noscript",
-            'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name',
+      "style",
-            'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields',
+      "textarea",
-            'constructor', 'constructors', 'instances'
+      "pre",
-        ],
+      "code",
-        ignoreHtmlClass: 'tex2jax_ignore',
+      "annotation",
-        processHtmlClass: 'tex2jax_process',
+      "annotation-xml",
-    },
+      "decl",
-};
+      "decl_meta",
+      "attributes",
+      "decl_args",
+      "decl_header",
+      "decl_name",
+      "decl_type",
+      "equation",
+      "equations",
+      "structure_field",
+      "structure_fields",
+      "constructor",
+      "constructors",
+      "instances",
+    ],
+    ignoreHtmlClass: "tex2jax_ignore",
+    processHtmlClass: "tex2jax_process",
+  },
+};

static/nav.js

@@ -1,248 +1,43 @@
-// Persistent expansion cookie for the file tree
+/**
-// ---------------------------------------------
+ * This module is used to implement persistent navbar expansion.
+ */
 
+// The variable to store the expansion information.
 let expanded = {};
-for (const e of (sessionStorage.getItem('expanded') || '').split(',')) {
+
-  if (e !== '') {
+// Load expansion information from sessionStorage.
+for (const e of (sessionStorage.getItem("expanded") || "").split(",")) {
+  if (e !== "") {
     expanded[e] = true;
   }
 }
 
+/**
+ * Save expansion information to sessionStorage.
+ */
 function saveExpanded() {
-  sessionStorage.setItem("expanded",
+  sessionStorage.setItem(
-    Object.getOwnPropertyNames(expanded).filter((e) => expanded[e]).join(","));
+    "expanded",
+    Object.getOwnPropertyNames(expanded)
+      .filter((e) => expanded[e])
+      .join(",")
+  );
 }
 
-for (const elem of document.getElementsByClassName('nav_sect')) {
+// save expansion information when user change the expansion.
-  const id = elem.getAttribute('data-path');
+for (const elem of document.getElementsByClassName("nav_sect")) {
+  const id = elem.getAttribute("data-path");
   if (!id) continue;
   if (expanded[id]) {
     elem.open = true;
   }
-  elem.addEventListener('toggle', () => {
+  elem.addEventListener("toggle", () => {
     expanded[id] = elem.open;
     saveExpanded();
   });
 }
 
-for (const currentFileLink of document.getElementsByClassName('visible')) {
+// Scroll to center.
-  currentFileLink.scrollIntoView({block: 'center'});
+for (const currentFileLink of document.getElementsByClassName("visible")) {
-}
+  currentFileLink.scrollIntoView({ block: "center" });
-
+}
-
-
-
-
-
-// Tactic list tag filter
-// ----------------------
-
-function filterSelectionClass(tagNames, classname) {
-    if (tagNames.length == 0) {
-      for (const elem of document.getElementsByClassName(classname)) {
-        elem.classList.remove("hide");
-      }
-    } else {
-      // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
-      for (const elem of document.getElementsByClassName(classname)) {
-        elem.classList.add("hide");
-        for (const tagName of tagNames) {
-            if (elem.classList.contains(tagName)) {
-              elem.classList.remove("hide");
-            }
-        }
-      }
-    }
-  }
-
-  function filterSelection(c) {
-    filterSelectionClass(c, "tactic");
-    filterSelectionClass(c, "taclink");
-  }
-
-var filterBoxes = document.getElementsByClassName("tagfilter");
-
-function updateDisplay() {
-    filterSelection(getSelectValues());
-}
-
-function getSelectValues() {
-    var result = [];
-
-    for (const opt of filterBoxes) {
-
-      if (opt.checked) {
-        result.push(opt.value);
-      }
-    }
-    return result;
-  }
-
-function setSelectVal(val) {
-  for (const opt of filterBoxes) {
-    opt.checked = val;
-  }
-}
-
-updateDisplay();
-
-for (const opt of filterBoxes) {
-  opt.addEventListener('change', updateDisplay);
-}
-
-const tse = document.getElementById("tagfilter-selectall")
-if (tse != null) {
-  tse.addEventListener('change', function() {
-    setSelectVal(this.checked);
-    updateDisplay();
-  });
-}
-
-
-
-
-
-
-// Simple declaration search
-// -------------------------
-
-const declURL = new URL(`${siteRoot}searchable_data.bmp`, window.location);
-const getDecls = (() => {
-  let decls;
-  return () => {
-    if (!decls) decls = new Promise((resolve, reject) => {
-        const req = new XMLHttpRequest();
-        req.responseType = 'json';
-        req.addEventListener('load', () => resolve(loadDecls(req.response)));
-        req.addEventListener('error', () => reject());
-        req.open('GET', declURL);
-        req.send();
-      })
-    return decls;
-  }
-})()
-
-const declSearch = async (q) => getMatches(await getDecls(), q);
-
-const srId = 'search_results';
-document.getElementById('search_form')
-  .appendChild(document.createElement('div'))
-  .id = srId;
-
-function handleSearchCursorUpDown(down) {
-  const sel = document.querySelector(`#${srId} .selected`);
-  const sr = document.getElementById(srId);
-  if (sel) {
-    sel.classList.remove('selected');
-    const toSelect = down ?
-      sel.nextSibling || sr.firstChild:
-      sel.previousSibling || sr.lastChild;
-    toSelect && toSelect.classList.add('selected');
-  } else {
-    const toSelect = down ? sr.firstChild : sr.lastChild;
-    toSelect && toSelect.classList.add('selected');
-  }
-}
-
-function handleSearchEnter() {
-  const sel = document.querySelector(`#${srId} .selected`)
-    || document.getElementById(srId).firstChild;
-  sel.click();
-}
-
-const searchInput = document.querySelector('#search_form input[name=q]');
-
-searchInput.addEventListener('keydown', (ev) => {
-  switch (ev.key) {
-    case 'Down':
-    case 'ArrowDown':
-      ev.preventDefault();
-      handleSearchCursorUpDown(true);
-      break;
-    case 'Up':
-    case 'ArrowUp':
-      ev.preventDefault();
-      handleSearchCursorUpDown(false);
-      break;
-    case 'Enter':
-      ev.preventDefault();
-      handleSearchEnter();
-      break;
-  }
-});
-
-searchInput.addEventListener('input', async (ev) => {
-  const text = ev.target.value;
-
-  if (!text) {
-    const sr = document.getElementById(srId);
-    sr.removeAttribute('state');
-    sr.replaceWith(sr.cloneNode(false));
-    return;
-  }
-
-  document.getElementById(srId).setAttribute('state', 'loading');
-
-  const result = await declSearch(text);
-  if (ev.target.value != text) return;
-
-  const oldSR = document.getElementById('search_results');
-  const sr = oldSR.cloneNode(false);
-  for (const {decl} of result) {
-    const d = sr.appendChild(document.createElement('a'));
-    d.innerText = decl;
-    d.title = decl;
-    d.href = `${siteRoot}find/${decl}`;
-  }
-  sr.setAttribute('state', 'done');
-  oldSR.replaceWith(sr);
-});
-
-
-
-
-
-
-// 404 page goodies
-// ----------------
-
-const howabout = document.getElementById('howabout');
-if (howabout) {
-  howabout.innerText = "Please wait a second.  I'll try to help you.";
-
-  howabout.parentNode
-      .insertBefore(document.createElement('pre'), howabout)
-      .appendChild(document.createElement('code'))
-      .innerText = window.location.href.replace(/[/]/g, '/\u200b');
-
-  const query = window.location.href.match(/[/]([^/]+)(?:\.html|[/])?$/)[1];
-  declSearch(query).then((results) => {
-      howabout.innerText = 'How about one of these instead:';
-      const ul = howabout.appendChild(document.createElement('ul'));
-      for (const {decl} of results) {
-          const li = ul.appendChild(document.createElement('li'));
-          const a = li.appendChild(document.createElement('a'));
-          a.href = `${siteRoot}find/${decl}`;
-          a.appendChild(document.createElement('code')).innerText = decl;
-      }
-  });
-}
-
-
-
-
-
-
-// Rewrite GitHub links
-// --------------------
-
-for (const elem of document.getElementsByClassName('gh_link')) {
-  const a = elem.firstElementChild;
-  // commit is set in add_commit.js
-  for (const [prefix, replacement] of commit) {
-    if (a.href.startsWith(prefix)) {
-      a.href = a.href.replace(prefix, replacement);
-      break;
-    }
-  }
-}

static/search.js

@@ -1,51 +1,118 @@
-function isSep(c) {
+/**
-    return c === '.' || c === '_';
+ * This module is used to handle user's interaction with the search form.
+ */
+
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+const SEARCH_FORM = document.querySelector("#search_form");
+const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]");
+
+// Create an `div#search_results` to hold all search results.
+let sr = document.createElement("div");
+sr.id = "search_results";
+SEARCH_FORM.appendChild(sr);
+
+/**
+ * Attach `selected` class to the the selected search result.
+ */
+function handleSearchCursorUpDown(down) {
+  const sel = sr.querySelector(`.selected`);
+  if (sel) {
+    sel.classList.remove("selected");
+    const toSelect = down
+      ? sel.nextSibling || sr.firstChild
+      : sel.previousSibling || sr.lastChild;
+    toSelect && toSelect.classList.add("selected");
+  } else {
+    const toSelect = down ? sr.firstChild : sr.lastChild;
+    toSelect && toSelect.classList.add("selected");
+  }
 }
 
-function matchCaseSensitive(declName, lowerDeclName, pat) {
+/**
-    let i = 0, j = 0, err = 0, lastMatch = 0
+ * Perform search (when enter is pressed).
-    while (i < declName.length && j < pat.length) {
+ */
-        if (pat[j] === declName[i] || pat[j] === lowerDeclName[i]) {
+function handleSearchEnter() {
-            err += (isSep(pat[j]) ? 0.125 : 1) * (i - lastMatch);
+  const sel = sr.querySelector(`.selected`) || sr.firstChild;
-            if (pat[j] !== declName[i]) err += 0.5;
+  sel.click();
-            lastMatch = i + 1;
+}
-            j++;
+
-        } else if (isSep(declName[i])) {
+/**
-            err += 0.125 * (i + 1 - lastMatch);
+ * Allow user to navigate search results with up/down arrow keys, and choose with enter.
-            lastMatch = i + 1;
+ */
-        }
+SEARCH_INPUT.addEventListener("keydown", (ev) => {
-        i++;
+  switch (ev.key) {
-    }
+    case "Down":
-    err += 0.125 * (declName.length - lastMatch);
+    case "ArrowDown":
-    if (j === pat.length) {
+      ev.preventDefault();
-        return err;
+      handleSearchCursorUpDown(true);
+      break;
+    case "Up":
+    case "ArrowUp":
+      ev.preventDefault();
+      handleSearchCursorUpDown(false);
+      break;
+    case "Enter":
+      ev.preventDefault();
+      handleSearchEnter();
+      break;
+  }
+});
+
+/**
+ * Remove all children of a DOM node.
+ */
+function removeAllChildren(node) {
+  while (node.firstChild) {
+    node.removeChild(node.lastChild);
+  }
+}
+
+/**
+ * Handle user input and perform search.
+ */
+function handleSearch(dataCenter, err, ev) {
+  const text = ev.target.value;
+
+  // If no input clear all.
+  if (!text) {
+    sr.removeAttribute("state");
+    removeAllChildren(sr);
+    return;
+  }
+
+  // searching
+  sr.setAttribute("state", "loading");
+
+  if (dataCenter) {
+    const result = dataCenter.search(text, false);
+
+    // in case user has updated the input.
+    if (ev.target.value != text) return;
+  
+    // update search results
+    removeAllChildren(sr);
+    for (const { name, docLink } of result) {
+      const d = sr.appendChild(document.createElement("a"));
+      d.innerText = name;
+      d.title = name;
+      d.href = docLink;
     }
+  }
+  // handle error
+  else {
+    removeAllChildren(sr);
+    const d = sr.appendChild(document.createElement("a"));
+    d.innerText = `Cannot fetch data, please check your network connection.\n${err}`;
+  }
+  sr.setAttribute("state", "done");
 }
 
-function loadDecls(searchableDataCnt) {
+DeclarationDataCenter.init()
-    return searchableDataCnt.map(({name, description}) => [name, name.toLowerCase(), description.toLowerCase()])
+  .then((dataCenter) => {
-}
+    // Search autocompletion.
-
+    SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev));
-function getMatches(decls, pat, maxResults = 30) {
+  })
-    const lowerPats = pat.toLowerCase().split(/\s/g);
+  .catch(e => {
-    const patNoSpaces = pat.replace(/\s/g, '');
+    SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev));
-    const results = [];
+  });
-    for (const [decl, lowerDecl, lowerDoc] of decls) {
-        let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces);
-
-        // match all words as substrings of docstring
-        if (!(err < 3) && pat.length > 3 && lowerPats.every(l => lowerDoc.indexOf(l) != -1)) {
-            err = 3;
-        }
-
-        if (err !== undefined) {
-            results.push({decl, err});
-        }
-    }
-    return results.sort(({err: a}, {err: b}) => a - b).slice(0, maxResults);
-}
-
-if (typeof process === 'object') { // NodeJS
-    const data = loadDecls(JSON.parse(require('fs').readFileSync('searchable_data.bmp').toString()));
-    console.log(getMatches(data, process.argv[2] || 'ltltle'));
-}

static/site-root.js

@@ -0,0 +1,4 @@
+/**
+ * Get the site root, {siteRoot} is to be replaced by doc-gen4.
+ */
+export const SITE_ROOT = "{siteRoot}";

static/style.css

@@ -273,10 +273,15 @@ nav {
     margin-top: 1ex;
 }
 
-.nav details, .nav_link {
+.nav details > * {
     padding-left: 2ex;
 }
 
+.nav summary {
+    cursor: pointer;
+    padding-left: 0;
+}
+
 .nav summary::marker {
     font-size: 85%;
 }
@@ -294,6 +299,10 @@ nav {
     overflow-wrap: break-word;
 }
 
+.nav_link {
+    overflow-wrap: break-word;
+}
+
 .decl > div, .mod_doc {
     padding-left: 8px;
     padding-right: 8px;

static/tactic.js

@@ -0,0 +1,61 @@
+// TODO: The tactic part seem to be unimplemented now.
+
+function filterSelectionClass(tagNames, classname) {
+  if (tagNames.length == 0) {
+    for (const elem of document.getElementsByClassName(classname)) {
+      elem.classList.remove("hide");
+    }
+  } else {
+    // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
+    for (const elem of document.getElementsByClassName(classname)) {
+      elem.classList.add("hide");
+      for (const tagName of tagNames) {
+        if (elem.classList.contains(tagName)) {
+          elem.classList.remove("hide");
+        }
+      }
+    }
+  }
+}
+
+function filterSelection(c) {
+  filterSelectionClass(c, "tactic");
+  filterSelectionClass(c, "taclink");
+}
+
+var filterBoxes = document.getElementsByClassName("tagfilter");
+
+function updateDisplay() {
+  filterSelection(getSelectValues());
+}
+
+function getSelectValues() {
+  var result = [];
+
+  for (const opt of filterBoxes) {
+    if (opt.checked) {
+      result.push(opt.value);
+    }
+  }
+  return result;
+}
+
+function setSelectVal(val) {
+  for (const opt of filterBoxes) {
+    opt.checked = val;
+  }
+}
+
+updateDisplay();
+
+for (const opt of filterBoxes) {
+  opt.addEventListener("change", updateDisplay);
+}
+
+const tse = document.getElementById("tagfilter-selectall");
+if (tse != null) {
+  tse.addEventListener("change", function () {
+    setSelectVal(this.checked);
+    updateDisplay();
+  });
+}