-
Notifications
You must be signed in to change notification settings - Fork 36
/
Structure.lean
51 lines (46 loc) · 1.56 KB
/
Structure.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
import DocGen4.Output.Template
import DocGen4.Output.DocString
import DocGen4.Process
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean
/--
Render a single field consisting of its documentation, its name and its type as HTML.
-/
def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
let shortName := f.name.componentsRev.head!.toString
let name := f.name.toString
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>
/--
Render all information about a structure as HTML.
-/
def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
let structureHtml :=
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.componentsRev.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>)
pure #[structureHtml]
end Output
end DocGen4