feat: export search.js info

DocGen4/Output.lean

@@ -65,6 +65,13 @@ 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
+  let mut declList := #[]
+  for (_, mod) in result.moduleInfo.toArray do
+    for decl in mod.members do
+      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

DocGen4/Output/Template.lean

@@ -49,6 +49,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
 
       -- TODO Add more js stuff
       <script src={s!"{←getRoot}nav.js"}></script>
+      <script src={s!"{←getRoot}search.js"}></script>
       </body>
     </html>
 

DocGen4/Process.lean

@@ -444,6 +444,17 @@ def getAttrs : DocInfo → Array String
 | classInfo i => i.attrs
 | classInductiveInfo i => i.attrs
 
+def getDocString : DocInfo → Option String
+| axiomInfo i => i.doc
+| theoremInfo i => i.doc
+| opaqueInfo i => i.doc
+| definitionInfo i => i.doc
+| instanceInfo i => i.doc
+| inductiveInfo i => i.doc
+| structureInfo i => i.doc
+| classInfo i => i.doc
+| classInductiveInfo i => i.doc
+
 end DocInfo
 
 structure AnalyzerResult where