diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
index fb6105d..8bc03e5 100644
--- a/DocGen4/Output/Structure.lean
+++ b/DocGen4/Output/Structure.lean
@@ -10,7 +10,18 @@ open Lean
def fieldToHtml (f : NameInfo) : HtmlM Html := do
let shortName := f.name.components'.head!.toString
let name := f.name.toString
- pure
{s!"{shortName} "} : [←infoFormatToHtml f.type]
+ if let some doc := f.doc then
+ let renderedDoc ← docStringToHtml doc
+ pure
+
+ [renderedDoc]
+ {s!"{shortName} "} : [←infoFormatToHtml f.type]
+
+ else
+ pure
+
+ {s!"{shortName} "} : [←infoFormatToHtml f.type]
+
def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
let structureHtml :=
diff --git a/static/style.css b/static/style.css
index d056b40..b6d7f34 100644
--- a/static/style.css
+++ b/static/style.css
@@ -460,7 +460,7 @@ main h2, main h3, main h4, main h5, main h6 {
margin-left: 4ex; /* extra indentation */
}
-.imports li, code, .decl_header, .attributes, .structure_field,
+.imports li, code, .decl_header, .attributes, .structure_field_info,
.constructor, .instances li, .equation, #search_results div,
.structure_ext_ctor {
font-family: 'Source Code Pro', monospace;
@@ -491,6 +491,11 @@ pre code { padding: 0 0; }
margin-left: 2ex;
}
+.structure_field_doc {
+ text-indent: 0;
+ padding-top: 1ex;
+}
+
.structure_ext_fields {
display: block;
padding-inline-start: 0;