From 4d63f90449cb0e3c507471215e926d15ee4ed3fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 2 Feb 2022 12:53:04 +0100
Subject: [PATCH] feat: Custom structure ctors

Add the ability to show customly named structure constructors as well
as a little cosmetic change to how structure fields are displayed.
---
 DocGen4/Output/Structure.lean | 17 +++++++++++++++--
 lean-toolchain                |  2 +-
 static/style.css              | 19 ++++++++++++++++++-
 3 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
index 2c5b76d..688324f 100644
--- a/DocGen4/Output/Structure.lean
+++ b/DocGen4/Output/Structure.lean
@@ -4,14 +4,27 @@ namespace DocGen4
 namespace Output
 
 open scoped DocGen4.Jsx
+open Lean
 
 def fieldToHtml (f : NameInfo) : HtmlM Html := do
   let shortName := f.name.components'.head!.toString
   let name := f.name.toString
-  return <li «class»="structure_field" id={name}>{shortName} : [←infoFormatToHtml f.type]</li>
+  return <li «class»="structure_field" id={name}>{s!"{shortName} "} : [←infoFormatToHtml f.type]</li>
 
 def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
-  #[Html.element "ul" false #[("class", "structure_fields"), ("id", s!"{i.name.toString}.mk")] (←i.fieldInfo.mapM fieldToHtml)]
+  if Name.isSuffixOf `mk i.ctor.name then
+    #[<ul «class»="structure_fields" id={i.ctor.name.toString}>
+      [←i.fieldInfo.mapM fieldToHtml]
+    </ul>]
+  else
+    let ctorShortName := i.ctor.name.components'.head!.toString
+    #[<ul «class»="structure_ext">
+        <li id={i.ctor.name.toString} «class»="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
+        <ul «class»="structure_ext_fields">
+          [←i.fieldInfo.mapM fieldToHtml]
+        </ul>
+        <li «class»="structure_ext_ctor">)</li>
+      </ul>]
 
 end Output
 end DocGen4
diff --git a/lean-toolchain b/lean-toolchain
index 19c9eec..42a3c93 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-01-16
+leanprover/lean4:nightly-2022-02-01
diff --git a/static/style.css b/static/style.css
index 958eb2f..7e28a65 100644
--- a/static/style.css
+++ b/static/style.css
@@ -455,7 +455,8 @@ main h2, main h3, main h4, main h5, main h6 {
 }
 
 .imports li, code, .decl_header, .attributes, .structure_field,
-        .constructor, .instances li, .equation, #search_results div {
+        .constructor, .instances li, .equation, #search_results div,
+        .structure_ext_ctor {
     font-family: 'Source Code Pro', monospace;
 }
 
@@ -484,6 +485,22 @@ pre code { padding: 0 0; }
     margin-left: 2ex;
 }
 
+.structure_ext_fields {
+    display: block;
+    padding-inline-start: 0;
+    margin-top: 1ex;
+    text-indent: -2ex; padding-left: 2ex;
+}
+
+.structure_ext_fields .structure_field {
+    margin-left: -1ex !important;
+}
+
+.structure_ext_ctor {
+    display: block;
+    text-indent: -3ex;
+}
+
 .constructor {
     display: block;
 }