diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean
index 64813d4..273d765 100644
--- a/DocGen4/Output/Definition.lean
+++ b/DocGen4/Output/Definition.lean
@@ -1,3 +1,4 @@
+import CMark
import DocGen4.Output.Template
namespace DocGen4
@@ -23,11 +24,14 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do
pure none
def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
- let equationsHtml ← equationsToHtml i
- if let some equationsHtml := equationsHtml then
- pure #[equationsHtml]
- else
- pure #[]
+ let equationsHtml? ← equationsToHtml i
+ let docstringHtml? := i.doc.map λ s => Html.text (CMark.renderHtml s)
+ match equationsHtml?, docstringHtml? with
+ | some e, some d => pure #[e, d]
+ | some e, none => pure #[e]
+ | none , some e => pure #[e]
+ | none , none => pure #[]
+
end Output
end DocGen4
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index d8f84df..43f61dd 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -1,3 +1,4 @@
+import CMark
import DocGen4.Output.Template
namespace DocGen4
@@ -11,7 +12,11 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do
pure
{shortName} : [←infoFormatToHtml i.type]
def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
- pure #[[← i.ctors.toArray.mapM ctorToHtml]
]
+ let constructorsHtml := [← i.ctors.toArray.mapM ctorToHtml]
+ let docstringHtml? := i.doc.map λ s => Html.text (CMark.renderHtml s)
+ match docstringHtml? with
+ | some d => pure #[constructorsHtml, d]
+ | none => pure #[constructorsHtml]
end Output
end DocGen4
diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
index 23212ae..4b8a330 100644
--- a/DocGen4/Output/Structure.lean
+++ b/DocGen4/Output/Structure.lean
@@ -1,3 +1,4 @@
+import CMark
import DocGen4.Output.Template
namespace DocGen4
@@ -12,21 +13,24 @@ def fieldToHtml (f : NameInfo) : HtmlM Html := do
pure {s!"{shortName} "} : [←infoFormatToHtml f.type]
def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
- if Name.isSuffixOf `mk i.ctor.name then
- pure #[
-
+ let structureHtml :=
+ if Name.isSuffixOf `mk i.ctor.name then
+ (
[←i.fieldInfo.mapM fieldToHtml]
-
]
- else
- let ctorShortName := i.ctor.name.components'.head!.toString
- pure #[
- )
+ else
+ let ctorShortName := i.ctor.name.components'.head!.toString
+ (
- {s!"{ctorShortName} "} :: (
[←i.fieldInfo.mapM fieldToHtml]
- )
-
]
+
)
+ let docstringHtml? := i.doc.map λ s => Html.text (CMark.renderHtml s)
+ match docstringHtml? with
+ | some d => pure #[structureHtml, d]
+ | none => pure #[structureHtml]
end Output
end DocGen4
diff --git a/lakefile.lean b/lakefile.lean
index 2f747bb..77e34d7 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,4 +4,10 @@ open Lake DSL
package «doc-gen4» {
-- add configuration options here
supportInterpreter := true
+ dependencies := #[
+ {
+ name := `CMark
+ src := Source.git "https://github.com/xubaiw/CMark.lean" "925f2ab"
+ }
+ ]
}