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

Merge pull request #17 from leanprover/sidebar-names 

Sidebar names
main
Henrik Böving 2022-01-07 18:29:01 +01:00 committed by GitHub
parent 82f63cb613 6128791cce
commit b90644cfd2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 46 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
DocGen4/Output/Module.lean
View File

@ -89,14 +89,26 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
</div> </div>
</div> </div>
def moduleToNavLink (module : Name) : Html :=
<div «class»="nav_link">
<a «class»="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
</div>
def internalNav (members : Array Name) (moduleName : Name) : Html :=
<nav «class»="internal_nav">
<h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
-- TODO: Proper source links
<p «class»="gh_nav_link"><a href="https://github.com">source</a></p>
[members.map moduleToNavLink]
</nav>
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? let docInfos ← module.members.mapM docInfoToHtml
-- maybe they should already be ordered in members. -- TODO: This is missing imports, imported by
let sortedMembers := module.members.qsort (λ l r => l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line) templateExtends (baseHtmlArray module.name.toString) $ #[
let docInfos ← sortedMembers.mapM docInfoToHtml internalNav (module.members.map DocInfo.getName) module.name,
-- TODO: This is missing imports, imported by, source link, list of decls
templateExtends (baseHtml module.name.toString) $
Html.element "main" false #[] docInfos Html.element "main" false #[] docInfos
]
end Output end Output
end DocGen4 end DocGen4

9
DocGen4/Output/Template.lean
View File

@ -11,7 +11,7 @@ namespace Output
open scoped DocGen4.Jsx open scoped DocGen4.Jsx
def baseHtml (title : String) (site : Html) : HtmlM Html := do def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
<html lang="en"> <html lang="en">
<head> <head>
<link rel="stylesheet" href={s!"{←getRoot}style.css"}/> <link rel="stylesheet" href={s!"{←getRoot}style.css"}/>
@ -37,9 +37,7 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do
</form> </form>
</header> </header>
<nav «class»="internal_nav"></nav> [site]
{site}
{←navbar} {←navbar}
@ -53,5 +51,8 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do
</body> </body>
</html> </html>
def baseHtml (title : String) (site : Html) : HtmlM Html := baseHtmlArray title #[site]
end Output end Output
end DocGen4 end DocGen4

33
DocGen4/Process.lean
View File

@ -77,9 +77,27 @@ inductive DocInfo where
| classInfo (info : ClassInfo) : DocInfo | classInfo (info : ClassInfo) : DocInfo
deriving Inhabited 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 structure Module where
name : Name name : Name
doc : Option String doc : Option String
-- Sorted according to their line numbers
members : Array DocInfo members : Array DocInfo
deriving Inhabited deriving Inhabited
@ -295,16 +313,6 @@ 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
@ -338,6 +346,11 @@ def process : MetaM AnalyzerResult := do
res := res.insert moduleName {module with members := module.members.push dinfo} res := res.insert moduleName {module with members := module.members.push dinfo}
| none => panic! "impossible" | none => panic! "impossible"
| none => () | 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 { return {
name2ModIdx := env.const2ModIdx, name2ModIdx := env.const2ModIdx,
moduleNames := env.header.moduleNames, moduleNames := env.header.moduleNames,