diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 44438b2..bb4ea87 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -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
+
+
+
+ -- TODO: Put the proper source link
+
source
+
+ -- TODO: Attributes
+ -- TODO: Noncomputable, partial etc.
+
{doc.getKind}
+ -- TODO: HTMLify the name etc.
+ {doc.getName.toString}
+ -- TODO: args
+ -- TODO: The actual type information we are here for
+
+
+
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) $
-
- This is the page of {module.name.toString}
-
+ Html.element "main" #[] docInfos
end Output
end DocGen4
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 950beac..b1bc9fc 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -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