r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

feat: show all declarations in the correct order 

Closes: #7
main
Henrik Böving 2022-01-06 17:30:33 +01:00
parent eae71c61a3
commit ec4d114b43
2 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
DocGen4/Output/Module.lean
View File

@ -92,7 +92,8 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
-- TODO: Probably some sort of ordering by line number would be cool? -- TODO: Probably some sort of ordering by line number would be cool?
-- maybe they should already be ordered in members. -- 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 -- TODO: This is missing imports, imported by, source link, list of decls
templateExtends (baseHtml module.name.toString) $ templateExtends (baseHtml module.name.toString) $
Html.element "main" false #[] docInfos Html.element "main" false #[] docInfos

10
DocGen4/Process.lean
View File

@ -295,6 +295,16 @@ def getArgs : DocInfo → Array Arg
| structureInfo i => i.args | structureInfo i => i.args
| classInfo 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 end DocInfo
structure AnalyzerResult where structure AnalyzerResult where