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

doc: Output.Navbar

main
Henrik Böving 2022-05-19 21:49:25 +02:00
parent 20e136bb27
commit 94ce87d11a
1 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
DocGen4/Output/Navbar.lean
View File

@ -18,6 +18,9 @@ def moduleListFile (file : Name) : HtmlM Html := do
{←moduleToHtmlLink file} {←moduleToHtmlLink file}
</div> </div>
/--
Build the HTML tree representing the module hierarchy.
-/
partial def moduleListDir (h : Hierarchy) : HtmlM Html := do partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
let children := Array.mk (h.getChildren.toList.map Prod.snd) let children := Array.mk (h.getChildren.toList.map Prod.snd)
let dirs := children.filter (λ c => c.getChildren.toList.length != 0) let dirs := children.filter (λ c => c.getChildren.toList.length != 0)
@ -39,6 +42,9 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
[fileNodes] [fileNodes]
</details> </details>
/--
Return a list of top level modules, linkified and rendered as HTML
-/
def moduleList : HtmlM Html := do def moduleList : HtmlM Html := do
let hierarchy := (←getResult).hierarchy let hierarchy := (←getResult).hierarchy
let mut list := Array.empty let mut list := Array.empty
@ -46,6 +52,9 @@ def moduleList : HtmlM Html := do
list := list.push $ ←moduleListDir cs list := list.push $ ←moduleListDir cs
pure <div class="module_list">[list]</div> pure <div class="module_list">[list]</div>
/--
The main entry point to rendering the navbar on the left hand side.
-/
def navbar : HtmlM Html := do def navbar : HtmlM Html := do
pure pure
<nav class="nav"> <nav class="nav">