Merge pull request #41 from xubaiw/navbar

Navbar

DocGen4/Output/Navbar.lean

@@ -14,7 +14,7 @@ open Lean
 open scoped DocGen4.Jsx
 
 def moduleListFile (file : Name) : HtmlM Html := do
-  pure <div "class"="nav_link" [if (← getCurrentName) == file then #[("visible", "")] else #[]]>
+  pure <div «class»={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
     <a href={← moduleNameToLink file}>{file.toString}</a>
   </div>
 
@@ -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>

static/style.css

@@ -273,10 +273,15 @@ nav {
     margin-top: 1ex;
 }
 
-.nav details, .nav_link {
+.nav details > * {
     padding-left: 2ex;
 }
 
+.nav summary {
+    cursor: pointer;
+    padding-left: 0;
+}
+
 .nav summary::marker {
     font-size: 85%;
 }
@@ -294,6 +299,10 @@ nav {
     overflow-wrap: break-word;
 }
 
+.nav_link {
+    overflow-wrap: break-word;
+}
+
 .decl > div, .mod_doc {
     padding-left: 8px;
     padding-right: 8px;