From c42db4328adc39d03a4f85c2a1fd79481fb56bbd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 13 Feb 2022 15:03:49 +0100
Subject: [PATCH] feat: export search.js info

---
 DocGen4/Output.lean          |  7 +++++++
 DocGen4/Output/Template.lean |  1 +
 DocGen4/Process.lean         | 11 +++++++++++
 3 files changed, 19 insertions(+)

diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 0af12bb..32fe8aa 100644
--- a/DocGen4/Output.lean
+++ b/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
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index 72727a8..b44aa81 100644
--- a/DocGen4/Output/Template.lean
+++ b/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>
 
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 8435845..286b79c 100644
--- a/DocGen4/Process.lean
+++ b/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