Merge pull request #26 from leanprover/custom-ctors

feat: Custom structure ctors

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-01-16
+leanprover/lean4:nightly-2022-02-01

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;
 }