From 2de568d5ca9f4e55c034735f5adef6f6a2e669e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 7 Jan 2022 17:43:49 +0100 Subject: [PATCH 1/2] feat: List of declarations in internal navbar --- DocGen4/Output/Module.lean | 21 +++++++++++++++++---- DocGen4/Output/Template.lean | 9 +++++---- 2 files changed, 22 insertions(+), 8 deletions(-) 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 From 6128791cce423e8ce344f93e91b0873b1a9b3219 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 7 Jan 2022 18:25:26 +0100 Subject: [PATCH 2/2] chore: Sort the declarations internally already --- DocGen4/Output/Module.lean | 5 ++--- DocGen4/Process.lean | 33 +++++++++++++++++++++++---------- 2 files changed, 25 insertions(+), 13 deletions(-) diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index c645b78..e66196b 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -103,11 +103,10 @@ def internalNav (members : Array Name) (moduleName : Name) : Html := def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do - let sortedMembers := module.members.qsort (λ l r => l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line) - let docInfos ← sortedMembers.mapM docInfoToHtml + let docInfos ← module.members.mapM docInfoToHtml -- TODO: This is missing imports, imported by templateExtends (baseHtmlArray module.name.toString) $ #[ - internalNav (sortedMembers.map DocInfo.getName) module.name, + internalNav (module.members.map DocInfo.getName) module.name, Html.element "main" false #[] docInfos ] diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 8627247..3839c3a 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -77,9 +77,27 @@ inductive DocInfo where | classInfo (info : ClassInfo) : DocInfo deriving Inhabited +namespace DocInfo + +def getDeclarationRange : DocInfo → DeclarationRange +| axiomInfo i => i.declarationRange +| theoremInfo i => i.declarationRange +| opaqueInfo i => i.declarationRange +| definitionInfo i => i.declarationRange +| instanceInfo i => i.declarationRange +| inductiveInfo i => i.declarationRange +| structureInfo i => i.declarationRange +| classInfo i => i.declarationRange + +def lineOrder (l r : DocInfo) : Bool := + l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line + +end DocInfo + structure Module where name : Name doc : Option String + -- Sorted according to their line numbers members : Array DocInfo deriving Inhabited @@ -295,16 +313,6 @@ def getArgs : DocInfo → Array Arg | structureInfo i => i.args | classInfo i => i.args -def getDeclarationRange : DocInfo → DeclarationRange -| axiomInfo i => i.declarationRange -| theoremInfo i => i.declarationRange -| opaqueInfo i => i.declarationRange -| definitionInfo i => i.declarationRange -| instanceInfo i => i.declarationRange -| inductiveInfo i => i.declarationRange -| structureInfo i => i.declarationRange -| classInfo i => i.declarationRange - end DocInfo structure AnalyzerResult where @@ -338,6 +346,11 @@ def process : MetaM AnalyzerResult := do res := res.insert moduleName {module with members := module.members.push dinfo} | none => panic! "impossible" | none => () + + -- This could probably be faster if we did an insertion sort above instead + for (moduleName, module) in res.toArray do + res := res.insert moduleName {module with members := module.members.qsort DocInfo.lineOrder} + return { name2ModIdx := env.const2ModIdx, moduleNames := env.header.moduleNames,