Merge pull request #24 from gebner/navbarheaders

fix: do not show top-level modules twice in navbar

DocGen4/Output/Inductive.lean

@@ -10,8 +10,8 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do
   let name := i.name.toString
   return <li «class»="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
 
-def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
-  #[Html.element "ul" false #[("class", "constructors")] (←i.ctors.toArray.mapM ctorToHtml)]
+def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) :=
+  return #[<ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>]
 
 end Output
 end DocGen4

DocGen4/Output/Navbar.lean

@@ -13,16 +13,10 @@ namespace Output
 open Lean
 open scoped DocGen4.Jsx
 
-def moduleListFile (file : Name) : HtmlM Html := do
-  let attributes := match ←getCurrentName with
-  | some name =>
-    if file == name then
-      #[("class", "nav_link"), ("visible", "")]
-    else
-      #[("class", "nav_link")]
-  | none => #[("class", "nav_link")]
-  let nodes := #[<a href={s!"{←moduleNameToLink file}"}>{file.toString}</a>]
-  return Html.element "div" false attributes nodes
+def moduleListFile (file : Name) : HtmlM Html :=
+  return <div "class"="nav_link" [if (← getCurrentName) == file then #[("visible", "")] else #[]]>
+    <a href={← moduleNameToLink file}>{file.toString}</a>
+  </div>
 
 partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   let children := Array.mk (h.getChildren.toList.map Prod.snd)
@@ -31,24 +25,19 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   let dirNodes ← (dirs.mapM moduleListDir)
   let fileNodes ← (files.mapM moduleListFile)
   let moduleLink ← moduleNameToLink h.getName
-  let attributes := match ←getCurrentName with
-  | some name =>
-    if h.getName.isPrefixOf name then
-      #[("class", "nav_sect"), ("data-path", moduleLink), ("open", "")]
-    else
-      #[("class", "nav_sect"), ("data-path", moduleLink)]
-  | none =>
-      #[("class", "nav_sect"), ("data-path", moduleLink)]
-  let nodes := #[<summary>{h.getName.toString}</summary>] ++ dirNodes ++ fileNodes
-  return Html.element "details" false attributes nodes
+  return <details "class"="nav_sect" "data-path"={moduleLink}
+      [if (← getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
+    <summary>{h.getName.toString}</summary>
+    [dirNodes]
+    [fileNodes]
+  </details>
 
-def moduleList : HtmlM (Array Html) := do
+def moduleList : HtmlM Html := do
   let hierarchy := (←getResult).hierarchy
   let mut list := Array.empty
   for (n, cs) in hierarchy.getChildren do
-    list := list.push <h4>{n.toString}</h4>
     list := list.push $ ←moduleListDir cs
-  list
+  return <div "class"="module_list">[list]</div>
 
 def navbar : HtmlM Html := do
   <nav «class»="nav">
@@ -64,7 +53,7 @@ def navbar : HtmlM Html := do
     <div «class»="nav_link"><a href={s!"{←getRoot}references.html"}>references</a></div>
     -/
     <h3>Library</h3>
-    [←moduleList]
+    {← moduleList}
   </nav>
 
 end Output

DocGen4/ToHtmlFormat.lean

@@ -53,9 +53,6 @@ open Parser PrettyPrinter
 declare_syntax_cat jsxElement
 declare_syntax_cat jsxChild
 
-def jsxAttrVal : Parser := strLit <|> group ("{" >> termParser >> "}")
-def jsxAttr : Parser := ident >> "=" >> jsxAttrVal
-
 -- JSXTextCharacter : SourceCharacter but not one of {, <, > or }
 def jsxText : Parser :=
   withAntiquot (mkAntiquot "jsxText" `jsxText) {
@@ -67,41 +64,57 @@ def jsxText : Parser :=
 @[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
 @[combinatorParenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
 
-scoped syntax "<" ident jsxAttr* "/>" : jsxElement
-scoped syntax "<" ident jsxAttr* ">" jsxChild* "</" ident ">" : jsxElement
+syntax jsxAttrName := ident <|> strLit
+syntax jsxAttrVal := strLit <|> group("{" term "}")
+syntax jsxSimpleAttr := jsxAttrName "=" jsxAttrVal
+syntax jsxAttrSpread := "[" term "]"
+syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
 
-scoped syntax jsxText      : jsxChild
-scoped syntax "{" term "}" : jsxChild
-scoped syntax "[" term "]" : jsxChild
-scoped syntax jsxElement   : jsxChild
+syntax "<" ident jsxAttr* "/>" : jsxElement
+syntax "<" ident jsxAttr* ">" jsxChild* "</" ident ">" : jsxElement
+
+syntax jsxText      : jsxChild
+syntax "{" term "}" : jsxChild
+syntax "[" term "]" : jsxChild
+syntax jsxElement   : jsxChild
 
 scoped syntax:max jsxElement : term
 
+def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
+  let mut as ← `(#[])
+  for attr in attrs do
+    as ← match attr with
+    | `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
+      let n ← match n with
+        | `(jsxAttrName| $n:strLit) => n
+        | `(jsxAttrName| $n:ident) => quote (toString n.getId)
+        | _ => Macro.throwUnsupported
+      let v ← match v with
+        | `(jsxAttrVal| {$v}) => v
+        | `(jsxAttrVal| $v:strLit) => v
+        | _ => Macro.throwUnsupported
+      `(($as).push ($n, ($v : String)))
+    | `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))
+    | _ => Macro.throwUnsupported
+  return as
+
 macro_rules
-  | `(<$n $[$ns = $vs]* />) =>
-    let ns := ns.map (quote <| toString ·.getId)
-    let vs := vs.map fun
-      | `(jsxAttrVal| $s:strLit) => s
-      | `(jsxAttrVal| { $t:term }) => t
-      | _ => unreachable!
-    `(Html.element $(quote <| toString n.getId) false #[ $[($ns, $vs)],* ] #[])
-  | `(<$n $[$ns = $vs]* >$cs*</$m>) =>
-    if n.getId == m.getId then do
-      let ns := ns.map (quote <| toString ·.getId)
-      let vs := vs.map fun
-        | `(jsxAttrVal| $s:strLit) => s
-        | `(jsxAttrVal| { $t:term }) => t
-        | _ => unreachable!
-      let cs ← cs.mapM fun
-        | `(jsxChild|$t:jsxText)    => `(#[Html.text $(quote t[0].getAtomVal!)])
-        -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
-        | `(jsxChild|{$t})          => `(#[$t])
-        | `(jsxChild|[$t])          => `($t)
-        | `(jsxChild|$e:jsxElement) => `(#[$e:jsxElement])
-        | _                         => unreachable!
-      let tag := toString n.getId
-      `(Html.element $(quote tag) false #[ $[($ns, $vs)],* ] (Array.foldl Array.append #[] #[ $[$cs],* ]))
-    else Macro.throwError ("expected </" ++ toString n.getId ++ ">")
+  | `(<$n $attrs* />) => do
+    `(Html.element $(quote (toString n.getId)) true $(← translateAttrs attrs) #[])
+  | `(<$n $attrs* >$children*</$m>) => do
+    unless n.getId == m.getId do
+      withRef m <| Macro.throwError s!"expected </{n.getId}>"
+    let mut cs ← `(#[])
+    for child in children do
+      cs ← match child with
+      | `(jsxChild|$t:jsxText)    => `(($cs).push (Html.text $(quote t[0].getAtomVal!)))
+      -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
+      | `(jsxChild|{$t})          => `(($cs).push ($t : Html))
+      | `(jsxChild|[$t])          => `($cs ++ ($t : Array Html))
+      | `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html))
+      | _                         => Macro.throwUnsupported
+    let tag := toString n.getId
+    `(Html.element $(quote tag) false $(← translateAttrs attrs) $cs)
 
 end Jsx
 

Main.lean

@@ -4,6 +4,10 @@ import Lean
 open DocGen4 Lean IO
 
 def main (args : List String) : IO Unit := do
+  if args.isEmpty then
+    IO.println "Usage: doc-gen4 root/url/ Module1 Module2 ..."
+    IO.Process.exit 1
+    return
   let root := args.head!
   let modules := args.tail!
   let path ← lakeSetupSearchPath (←getLakePath) modules.toArray

static/style.css

@@ -268,6 +268,11 @@ nav {
     margin-bottom: 1ex;
 }
 
+/* top-level modules in left navbar */
+.nav .module_list > details {
+    margin-top: 1ex;
+}
+
 .nav details > * {
     padding-left: 2ex;
 }
@@ -287,10 +292,6 @@ nav {
     margin-block-end: 4px;
 }
 
-.nav h4 {
-    margin-bottom: 1ex;
-}
-
 /* People use way too long declaration names. */
 .internal_nav, .decl_name {
     overflow-wrap: break-word;