From d8a5f52c101ac89c3445e028a5475752b64d52b6 Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Fri, 18 Feb 2022 11:28:44 +0800
Subject: [PATCH] fix: fix docstring order

---
 DocGen4/Output/Definition.lean |  9 +++------
 DocGen4/Output/Inductive.lean  |  5 +----
 DocGen4/Output/Module.lean     | 15 ++++++++-------
 DocGen4/Output/Structure.lean  |  5 +----
 4 files changed, 13 insertions(+), 21 deletions(-)

diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean
index 374c10c..7261c37 100644
--- a/DocGen4/Output/Definition.lean
+++ b/DocGen4/Output/Definition.lean
@@ -25,12 +25,9 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do
 
 def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
   let equationsHtml? ← equationsToHtml i
-  let docstringHtml? ← i.doc.mapM docStringToHtml
-  match equationsHtml?, docstringHtml? with
-  | some e, some d => pure (#[e] ++ d)
-  | some e, none   => pure #[e]
-  | none  , some d => pure d
-  | none  , none   => pure #[]
+  match equationsHtml? with
+  | some e => pure #[e]
+  | none   => pure #[]
 
 
 end Output
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 5535290..ab29718 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -13,10 +13,7 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do
 
 def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
   let constructorsHtml := <ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
-  let docstringHtml? ← i.doc.mapM docStringToHtml
-  match docstringHtml? with
-  | some d => pure (#[constructorsHtml] ++ d)
-  | none   => pure #[constructorsHtml]
+  pure #[constructorsHtml]
 
 end Output
 end DocGen4
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 394c509..5d41123 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -74,17 +74,17 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   pure <div «class»="decl_header"> [nodes] </div>
 
 def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
-  let docHtml ← match doc with
+  let docInfoHtml ← match doc with
   | DocInfo.inductiveInfo i => inductiveToHtml i
   | DocInfo.structureInfo i => structureToHtml i
   | DocInfo.classInfo i => classToHtml i
   | DocInfo.definitionInfo i => definitionToHtml i
   | DocInfo.instanceInfo i => instanceToHtml i
   | DocInfo.classInductiveInfo i => classInductiveToHtml i
-  | i => match i.getDocString with
-    | some d => pure (← docStringToHtml d)
-    | _ => pure #[]
-
+  | i => pure #[]
+  let docStringHtml ← match doc.getDocString with
+  | some s => docStringToHtml s
+  | none => pure #[]
   let attrs := doc.getAttrs
   let attrsHtml :=
     if attrs.size > 0 then
@@ -101,7 +101,8 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
         </div>
         [attrsHtml]
         {←docInfoHeader doc}
-        [docHtml]
+        [docStringHtml]
+        [docInfoHtml]
       </div>
     </div>
 
@@ -111,7 +112,7 @@ def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
       [←docStringToHtml mdoc.doc]
     </div>
 
-def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := 
+def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
   match member with
   | ModuleMember.docInfo d => docInfoToHtml module d
   | ModuleMember.modDoc d => modDocToHtml module d
diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
index ab6e4d5..fb6105d 100644
--- a/DocGen4/Output/Structure.lean
+++ b/DocGen4/Output/Structure.lean
@@ -27,10 +27,7 @@ def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
         </ul>
         <li «class»="structure_ext_ctor">)</li>
       </ul>)
-  let docstringHtml? ← i.doc.mapM docStringToHtml
-  match docstringHtml? with
-  | some d => pure (#[structureHtml] ++ d)
-  | none   => pure #[structureHtml]
+  pure #[structureHtml]
 
 end Output
 end DocGen4