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.
main
Henrik Böving 2022-02-02 12:53:04 +01:00
parent b1abc677a0
commit 4d63f90449
3 changed files with 34 additions and 4 deletions

View File

@ -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

View File

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

View File

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