From a7c00d95e603eae0c6b0f4470e2e75208fad5f6b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 9 Apr 2022 21:39:34 +0200
Subject: [PATCH] feat: Render doc comments for structure fields

---
 DocGen4/Output/Structure.lean | 13 ++++++++++++-
 static/style.css              |  7 ++++++-
 2 files changed, 18 insertions(+), 2 deletions(-)

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 <li «class»="structure_field" id={name}>{s!"{shortName} "} : [←infoFormatToHtml f.type]</li>
+  if let some doc := f.doc then
+    let renderedDoc ← docStringToHtml doc
+    pure
+      <li id={name} «class»="structure_field">
+        <div «class»="structure_field_doc">[renderedDoc]</div>
+        <div «class»="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
+      </li>
+  else
+    pure
+      <li id={name} «class»="structure_field">
+        <div «class»="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
+      </li>
 
 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;