feat: Implement the rest of search

DocGen4/Output.lean

@@ -9,6 +9,7 @@ import DocGen4.Output.Base
 import DocGen4.Output.Index
 import DocGen4.Output.Module
 import DocGen4.Output.NotFound
+import DocGen4.Output.Find
 
 namespace DocGen4
 
@@ -65,14 +66,21 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
   let basePath := FilePath.mk "./build/doc/"
   let indexHtml := ReaderT.run index config 
   let notFoundHtml := ReaderT.run notFound config
+  FS.createDirAll basePath
+  FS.createDirAll (basePath / "find")
+
   let mut declList := #[]
   for (_, mod) in result.moduleInfo.toArray do
     for decl in mod.members do
+      let findHtml := ReaderT.run (findRedirectHtml decl.getName) config
+      let findDir := basePath / "find" / decl.getName.toString
+      FS.createDirAll findDir
+      FS.writeFile (findDir / "index.html") findHtml.toString
       let obj := Json.mkObj [("name", decl.getName.toString), ("description", decl.getDocString.getD "")]
       declList := declList.push obj
   let json := Json.arr declList
+
   FS.writeFile (basePath / "searchable_data.bmp") json.compress
-  FS.createDirAll basePath
   FS.writeFile (basePath / "index.html") indexHtml.toString
   FS.writeFile (basePath / "style.css") styleCss
   FS.writeFile (basePath / "404.html") notFoundHtml.toString

DocGen4/Output/Find.lean

@@ -0,0 +1,15 @@
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+def findRedirectHtml (decl : Name) : HtmlM Html := do
+  let res ← getResult
+  let url ← declNameToLink decl
+  let contentString := s!"0;url={url}"
+  pure $ Html.element "meta" false #[("http-equiv", "refresh"), ("content", contentString)] #[]
+end Output
+end DocGen4