From 87f959e11dd6461c5661e694e79921bf30400e19 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 6 Jan 2022 14:28:41 +0100
Subject: [PATCH] feat: basic structure like information for classes

---
 DocGen4/Output/Class.lean  | 13 +++++++++++++
 DocGen4/Output/Module.lean |  9 +++++++--
 2 files changed, 20 insertions(+), 2 deletions(-)
 create mode 100644 DocGen4/Output/Class.lean

diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean
new file mode 100644
index 0000000..e514b20
--- /dev/null
+++ b/DocGen4/Output/Class.lean
@@ -0,0 +1,13 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Structure
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
+  structureToHtml i.toStructureInfo
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 37fade1..3f8a34e 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -6,6 +6,7 @@ Authors: Henrik Böving
 import DocGen4.Output.Template
 import DocGen4.Output.Inductive
 import DocGen4.Output.Structure
+import DocGen4.Output.Class
 
 namespace DocGen4
 namespace Output
@@ -59,8 +60,11 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   for arg in doc.getArgs do
     nodes := nodes.push (←argToHtml arg)
 
-  if let DocInfo.structureInfo i := doc then
-    nodes := nodes.append (←structureInfoHeader i)
+  -- TODO: dedup this
+  match doc with
+  | DocInfo.structureInfo i => nodes := nodes.append (←structureInfoHeader i)
+  | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i.toStructureInfo)
+  | _ => nodes := nodes
 
   nodes := nodes.push <span «class»="decl_args">:</span>
   nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
@@ -70,6 +74,7 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
   let doc_html ← match doc with
   | DocInfo.inductiveInfo i => inductiveToHtml i
   | DocInfo.structureInfo i => structureToHtml i
+  | DocInfo.classInfo i => classToHtml i
   | _ => #[]
 
   return <div «class»="decl" id={doc.getName.toString}>