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

Merge pull request #34 from xubaiw/parent-module-nav 

fix: add nav link to non leaf node modules
main
Henrik Böving 2022-02-18 22:34:57 +01:00 committed by GitHub
parent 2dac93d360 1ef736c014
commit bd9ab34655
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 5 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
DocGen4/Output/Navbar.lean
View File

@ -21,14 +21,15 @@ def moduleListFile (file : Name) : HtmlM Html := do
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)
let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName let files := children.filter (λ c => Hierarchy.isFile c ∧ c.getChildren.toList.length = 0)
|>.map Hierarchy.getName
let dirNodes ← (dirs.mapM moduleListDir) let dirNodes ← (dirs.mapM moduleListDir)
let fileNodes ← (files.mapM moduleListFile) let fileNodes ← (files.mapM moduleListFile)
let moduleLink ← moduleNameToLink h.getName let moduleLink ← moduleNameToLink h.getName
pure pure
<details "class"="nav_sect" "data-path"={moduleLink} <details "class"="nav_sect" "data-path"={moduleLink}
[if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]> [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
<summary>{h.getName.toString}</summary> {Html.element "summary" true #[] #[<a "href"={← moduleNameToLink h.getName}>{h.getName.toString}</a>]}
[dirNodes] [dirNodes]
[fileNodes] [fileNodes]
</details> </details>

7
static/style.css
View File

@ -273,13 +273,10 @@ nav {
margin-top: 1ex; margin-top: 1ex;
} }
.nav details > * { .nav details, .nav_link {
padding-left: 2ex; padding-left: 2ex;
} }
.nav summary {
cursor: pointer;
padding-left: 0;
}
.nav summary::marker { .nav summary::marker {
font-size: 85%; font-size: 85%;
} }