Merge remote-tracking branch 'upstream/main' into docstring

DocGen4/Output.lean

@@ -63,7 +63,7 @@ def sourceLinker : IO (Name → Option DeclarationRange → String) := do
 
 def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
   let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker}
-  let basePath := FilePath.mk "./build/doc/"
+  let basePath := FilePath.mk "." / "build" / "doc"
   let indexHtml := ReaderT.run index config 
   let notFoundHtml := ReaderT.run notFound config
   FS.createDirAll basePath

DocGen4/Output/Navbar.lean

@@ -21,14 +21,15 @@ def moduleListFile (file : Name) : HtmlM Html := do
 partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   let children := Array.mk (h.getChildren.toList.map Prod.snd)
   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 fileNodes ← (files.mapM moduleListFile)
   let moduleLink ← moduleNameToLink h.getName
   pure
     <details "class"="nav_sect" "data-path"={moduleLink}
       [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]
       [fileNodes]
     </details>

static/style.css

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