feat: An initial list of declarations and their kinds

main
Henrik Böving 2021-12-15 11:59:36 +01:00
parent 2adf5125c1
commit b019faf7ba
2 changed files with 43 additions and 3 deletions

View File

@ -11,11 +11,31 @@ namespace Output
open scoped DocGen4.Jsx
-- TODO: This is a mix of decl.j2 and decl_header.j2, there is tons of stuff still missing
def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
<div «class»="decl" id={doc.getName.toString}>
<div «class»={doc.getKind}>
<div «class»="gh_link">
-- TODO: Put the proper source link
<a href="https://github.com">source</a>
</div>
-- TODO: Attributes
-- TODO: Noncomputable, partial etc.
<span «class»="decl_kind">{doc.getKind}</span>
-- TODO: HTMLify the name etc.
{doc.getName.toString}
-- TODO: args
-- TODO: The actual type information we are here for
</div>
</div>
def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
-- TODO: Probably some sort of ordering by line number would be cool?
-- maybe they should already be ordered in members.
let docInfos ← module.members.mapM docInfoToHtml
-- TODO: This is missing imports, imported by, source link, list of decls
templateExtends (baseHtml module.name.toString) $
<main>
<h1>This is the page of {module.name.toString}</h1>
</main>
Html.element "main" #[] docInfos
end Output
end DocGen4

View File

@ -256,6 +256,26 @@ def prettyPrint (i : DocInfo) : CoreM String := do
let fieldString ← i.fieldInfo.mapM (NameInfo.prettyPrint ∘ FieldInfo.toNameInfo)
s!"class {←i.toNameInfo.prettyPrint} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}"
def getName : DocInfo → Name
| axiomInfo i => i.name
| theoremInfo i => i.name
| opaqueInfo i => i.name
| definitionInfo i => i.name
| instanceInfo i => i.name
| inductiveInfo i => i.name
| structureInfo i => i.name
| classInfo i => i.name
def getKind : DocInfo → String
| axiomInfo _ => "axiom"
| theoremInfo _ => "theorem"
| opaqueInfo _ => "constant"
| definitionInfo _ => "def"
| instanceInfo _ => "instance" -- TODO: This doesnt exist in CSS yet
| inductiveInfo _ => "inductive"
| structureInfo _ => "structure"
| classInfo _ => "class" -- TODO: This is handled as structure right now
end DocInfo
namespace Module