feat: Name linking

DocGen4/Output.lean

@@ -25,7 +25,7 @@ def htmlOutput (result : AnalyzerResult) : IO Unit := do
   FS.writeFile (basePath / "style.css") styleCss
   FS.writeFile (basePath / "404.html") notFoundHtml.toString
   FS.writeFile (basePath / "nav.js") navJs
-  for (module, content) in result.modules.toArray do
+  for (module, content) in result.moduleInfo.toArray do
     let moduleHtml := ReaderT.run (moduleToHtml content) config
     let path := moduleNameToFile basePath module
     FS.createDirAll $ moduleNameToDirectory basePath module

DocGen4/Output/Base.lean

@@ -30,10 +30,9 @@ def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : H
   new >>= base
 
 -- TODO: Change this to HtmlM and auto add the root URl
-def moduleNameToUrl (n : Name) : String :=
-    (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
-  where
-    parts := n.components.map Name.toString
+def moduleNameToLink (n : Name) : HtmlM String := do
+  let parts := n.components.map Name.toString
+  (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
 
 def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
     FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"

DocGen4/Output/Module.lean

@@ -15,13 +15,23 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean PrettyPrinter
 
+def declNameToLink (name : Name) : HtmlM String := do
+  let res ← getResult
+  let module := res.moduleNames[res.name2ModIdx.find! name]
+  (←moduleNameToLink module) ++ "#" ++ name.toString
+
 def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   let mut nodes := #[]
   -- TODO: noncomputable, partial
   -- TODO: Support all the kinds in CSS
   nodes := nodes.push <span «class»="decl_kind">{doc.getKind}</span>
-  -- TODO: HTMLify the name etc.
-  nodes := nodes.push <span «class»="name">doc.getName.toString</span>
+  nodes := nodes.push
+    <span «class»="decl_name">
+      <a «class»="break_within" href={←declNameToLink doc.getName}>
+        -- TODO: HTMLify the name
+        {doc.getName.toString}
+      </a>
+    </span>
   -- TODO: Figure out how we can get explicit, implicit and TC args and put them here
   nodes := nodes.push <span «class»="decl_args">:</span>
   nodes := nodes.push <div «class»="decl_type"><span «class»="fn">Type!!!</span></div>

DocGen4/Output/Navbar.lean

@@ -21,7 +21,7 @@ def moduleListFile (file : Name) : HtmlM Html := do
     else
       #[("class", "nav_link")]
   | none => #[("class", "nav_link")]
-  let nodes := #[<a href={s!"{←getRoot}{moduleNameToUrl file}"}>{file.toString}</a>]
+  let nodes := #[<a href={s!"{←moduleNameToLink file}"}>{file.toString}</a>]
   return Html.element "div" attributes nodes
 
 partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
@@ -30,14 +30,15 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName
   let dirNodes ← (dirs.mapM moduleListDir)
   let fileNodes ← (files.mapM moduleListFile)
+  let moduleLink ← moduleNameToLink h.getName
   let attributes := match ←getCurrentName with
   | some name =>
     if h.getName.isPrefixOf name then
-      #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName), ("open", "")]
+      #[("class", "nav_sect"), ("data-path", moduleLink), ("open", "")]
     else
-      #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName)]
+      #[("class", "nav_sect"), ("data-path", moduleLink)]
   | none =>
-      #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName)]
+      #[("class", "nav_sect"), ("data-path", moduleLink)]
   let nodes := #[<summary>{h.getName.toString}</summary>] ++ dirNodes ++ fileNodes
   return Html.element "details" attributes nodes
 

DocGen4/Process.lean

@@ -290,7 +290,9 @@ def prettyPrint (m : Module) : CoreM String := do
 end Module
 
 structure AnalyzerResult where
-  modules : HashMap Name Module
+  name2ModIdx : HashMap Name ModuleIdx
+  moduleNames : Array Name
+  moduleInfo : HashMap Name Module
   hierarchy : Hierarchy
   deriving Inhabited
 
@@ -318,6 +320,11 @@ def process : MetaM AnalyzerResult := do
         res := res.insert moduleName {module with members := module.members.push dinfo}
       | none => panic! "impossible"
     | none => ()
-  return { modules := res, hierarchy := Hierarchy.fromArray env.header.moduleNames }
+  return {
+    name2ModIdx := env.const2ModIdx,
+    moduleNames := env.header.moduleNames,
+    moduleInfo := res,
+    hierarchy := Hierarchy.fromArray env.header.moduleNames
+  }
 
 end DocGen4