diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 0a05403..0aa9444 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -10,8 +10,8 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do
let name := i.name.toString
return
{shortName} : [←infoFormatToHtml i.type]
-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 #[[← i.ctors.toArray.mapM ctorToHtml]
]
end Output
end DocGen4
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index 6a2e07a..c94b6d9 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/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 := #[{file.toString}]
- return Html.element "div" false attributes nodes
+def moduleListFile (file : Name) : HtmlM Html :=
+ return
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 := #[{h.getName.toString}] ++ dirNodes ++ fileNodes
- return Html.element "details" false attributes nodes
+ return
+ {h.getName.toString}
+ [dirNodes]
+ [fileNodes]
+
def moduleList : HtmlM (Array Html) := do
let hierarchy := (←getResult).hierarchy
diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean
index c44f5be..253de07 100644
--- a/DocGen4/ToHtmlFormat.lean
+++ b/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