From 601b895e8973dbbf7a83a49eef56ab2b1ae4293a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 21 Jul 2022 20:23:27 +0200
Subject: [PATCH 1/2] feat: Inductive constructor doc strings

---
 DocGen4/Output/Inductive.lean | 19 +++++++++++++++----
 static/style.css              |  5 +++++
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 4a73bd3..47dbcaa 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -7,10 +7,21 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
-def ctorToHtml (i : Process.NameInfo) : HtmlM Html := do
-  let shortName := i.name.components'.head!.toString
-  let name := i.name.toString
-  pure <li class="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
+def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
+  let shortName := c.name.components'.head!.toString
+  let name := c.name.toString
+  if let some doc := c.doc then
+    let renderedDoc ← docStringToHtml doc
+    pure
+      <li class="constructor" id={name}>
+        <div class="inductive_ctor_doc">[renderedDoc]</div>
+        {shortName} : [←infoFormatToHtml c.type]
+      </li>
+  else
+    pure
+      <li class="constructor" id={name}>
+        {shortName} : [←infoFormatToHtml c.type]
+      </li>
 
 def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
   let constructorsHtml := <ul class="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
diff --git a/static/style.css b/static/style.css
index 85d0362..fbf8614 100644
--- a/static/style.css
+++ b/static/style.css
@@ -491,6 +491,11 @@ pre code { padding: 0 0; }
     margin-left: 2ex;
 }
 
+.inductive_ctor_doc  {
+    text-indent: 2ex;
+    padding-top: 1ex;
+}
+
 .structure_field_doc {
     text-indent: 0;
     padding-top: 1ex;

From ddaf76a401b4b7a9d9e41e31dde0cae4b950cf83 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 21 Jul 2022 20:27:54 +0200
Subject: [PATCH 2/2] chore: remove unused code

---
 Main.lean | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/Main.lean b/Main.lean
index e4f7bd0..2ea998e 100644
--- a/Main.lean
+++ b/Main.lean
@@ -20,18 +20,6 @@ def getTopLevelModules (p : Parsed) : IO (List String) :=  do
     throw $ IO.userError "No topLevelModules provided."
   pure topLevelModules
 
-def runInitCmd (p : Parsed) : IO UInt32 := do
-  let topLevelModules ← getTopLevelModules p
-  let res ← lakeSetup topLevelModules
-  match res with
-  | Except.ok _ =>
-    let modules := topLevelModules.map Name.mkSimple
-    let hierarchy ← loadInit modules
-    let baseConfig := getSimpleBaseContext hierarchy
-    htmlOutputSetup baseConfig
-    pure 0
-  | Except.error rc => pure rc
-
 def runSingleCmd (p : Parsed) : IO UInt32 := do
     let topLevelModules ← getTopLevelModules p
     let relevantModules := [p.positionalArg! "module" |>.as! String]