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

feat: short names in side bar

main
Henrik Böving 2022-12-13 18:58:02 +01:00
parent 84a116ac43
commit 327fdf0ddd
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
DocGen4/Output/Base.lean
View File

@ -108,7 +108,7 @@ def moduleNameToLink (n : Name) : BaseHtmlM String := do
Returns the HTML doc-gen4 link to a module name. Returns the HTML doc-gen4 link to a module name.
-/ -/
def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do
pure <a href={←moduleNameToLink module}>{module.toString}</a> pure <a href={←moduleNameToLink module}>{module.getString!}</a>
/-- /--
Returns the LeanInk link to a module name. Returns the LeanInk link to a module name.

2
DocGen4/Output/Navbar.lean
View File

@ -33,7 +33,7 @@ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
if h.isFile then if h.isFile then
<summary>{←moduleToHtmlLink h.getName}</summary> <summary>{←moduleToHtmlLink h.getName}</summary>
else else
<summary>{h.getName.toString}</summary> <summary>{h.getName.getString!}</summary>
pure pure
<details class="nav_sect" "data-path"={moduleLink} [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]> <details class="nav_sect" "data-path"={moduleLink} [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>