diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 3f8a34e..0aa91f8 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -92,7 +92,8 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do 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 + 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) $ Html.element "main" false #[] docInfos diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 19f6c2a..8627247 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -295,6 +295,16 @@ 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