feat: basic structure like information for classes

main
Henrik Böving 2022-01-06 14:28:41 +01:00
parent e67ea1d1f0
commit 87f959e11d
2 changed files with 20 additions and 2 deletions

13
DocGen4/Output/Class.lean Normal file
View File

@ -0,0 +1,13 @@
import DocGen4.Output.Template
import DocGen4.Output.Structure
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
structureToHtml i.toStructureInfo
end Output
end DocGen4

View File

@ -6,6 +6,7 @@ Authors: Henrik Böving
import DocGen4.Output.Template import DocGen4.Output.Template
import DocGen4.Output.Inductive import DocGen4.Output.Inductive
import DocGen4.Output.Structure import DocGen4.Output.Structure
import DocGen4.Output.Class
namespace DocGen4 namespace DocGen4
namespace Output namespace Output
@ -59,8 +60,11 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
for arg in doc.getArgs do for arg in doc.getArgs do
nodes := nodes.push (←argToHtml arg) nodes := nodes.push (←argToHtml arg)
if let DocInfo.structureInfo i := doc then -- TODO: dedup this
nodes := nodes.append (←structureInfoHeader i) match doc with
| DocInfo.structureInfo i => nodes := nodes.append (←structureInfoHeader i)
| DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i.toStructureInfo)
| _ => nodes := nodes
nodes := nodes.push <span «class»="decl_args">:</span> nodes := nodes.push <span «class»="decl_args">:</span>
nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType) nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
@ -70,6 +74,7 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
let doc_html ← match doc with let doc_html ← match doc with
| DocInfo.inductiveInfo i => inductiveToHtml i | DocInfo.inductiveInfo i => inductiveToHtml i
| DocInfo.structureInfo i => structureToHtml i | DocInfo.structureInfo i => structureToHtml i
| DocInfo.classInfo i => classToHtml i
| _ => #[] | _ => #[]
return <div «class»="decl" id={doc.getName.toString}> return <div «class»="decl" id={doc.getName.toString}>