From a5dfba5f1ccc840a0946f7bd23d3c6bf8e133068 Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Wed, 23 Feb 2022 23:09:10 +0800
Subject: [PATCH 1/3] fix: fix navbar centering

---
 DocGen4/Output/Navbar.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index efc9735..e56aa38 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/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>
 

From a50ca857aaf8219504f7b16154e891e950a2506a Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Wed, 23 Feb 2022 23:28:15 +0800
Subject: [PATCH 2/3] fix: wrap navbar overflow

---
 static/style.css | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/static/style.css b/static/style.css
index a4e0c9a..d056b40 100644
--- a/static/style.css
+++ b/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;

From dca4e42665f6c4d126fcbe9fb993f7bdb3f2a495 Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Wed, 23 Feb 2022 23:33:34 +0800
Subject: [PATCH 3/3] fix: filter out nonexist modules

---
 DocGen4/Output/Navbar.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index e56aa38..1a75288 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -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>