chore: use attribute spreads

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,16 +25,12 @@ 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
   let hierarchy := (←getResult).hierarchy

DocGen4/ToHtmlFormat.lean

@@ -93,7 +93,7 @@ def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
         | `(jsxAttrVal| {$v}) => v
         | `(jsxAttrVal| $v:strLit) => v
         | _ => Macro.throwUnsupported
-      `(($as).push ($n, $v))
+      `(($as).push ($n, ($v : String)))
     | `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))
     | _ => Macro.throwUnsupported
   return as