diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 0aa91f8..c645b78 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -89,14 +89,27 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do +def moduleToNavLink (module : Name) : Html := +
+ {module.toString} +
+ +def internalNav (members : Array Name) (moduleName : Name) : Html := + + 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 sortedMembers := module.members.qsort (λ l r => l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line) let docInfos ← sortedMembers.mapM docInfoToHtml - -- TODO: This is missing imports, imported by, source link, list of decls - templateExtends (baseHtml module.name.toString) $ + -- TODO: This is missing imports, imported by + templateExtends (baseHtmlArray module.name.toString) $ #[ + internalNav (sortedMembers.map DocInfo.getName) module.name, Html.element "main" false #[] docInfos + ] end Output end DocGen4 diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 5d82257..a22e9d6 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -11,7 +11,7 @@ namespace Output open scoped DocGen4.Jsx -def baseHtml (title : String) (site : Html) : HtmlM Html := do +def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do @@ -37,9 +37,7 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do - - - {site} + [site] {←navbar} @@ -53,5 +51,8 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do + +def baseHtml (title : String) (site : Html) : HtmlM Html := baseHtmlArray title #[site] + end Output end DocGen4