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

fix: filter out nonexist modules

main
Xubai Wang 2022-02-23 23:33:34 +08:00
parent a50ca857aa
commit dca4e42665
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
DocGen4/Output/Navbar.lean
View File

@ -29,7 +29,12 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
pure
<details "class"="nav_sect" "data-path"={moduleLink}
[if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
{Html.element "summary" true #[] #[<a "href"={← moduleNameToLink h.getName}>{h.getName.toString}</a>]}
{
if (←getResult).moduleInfo.contains h.getName then
Html.element "summary" true #[] #[<a "href"={← moduleNameToLink h.getName}>{h.getName.toString}</a>]
else
<summary>{h.getName.toString}</summary>
}
[dirNodes]
[fileNodes]
</details>