From 1ef736c014e9e98d7b2c0d932a5b35128821e6de Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Sat, 19 Feb 2022 02:07:25 +0800
Subject: [PATCH] fix: use flattened Html element

---
 DocGen4/Output/Navbar.lean | 2 +-
 DocGen4/ToHtmlFormat.lean  | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index 1b8a530..efc9735 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -29,7 +29,7 @@ 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 #[]]>
-      <summary><a "href"={← moduleNameToLink h.getName}>{h.getName.toString}</a></summary>
+      {Html.element "summary" true #[] #[<a "href"={← moduleNameToLink h.getName}>{h.getName.toString}</a>]}
       [dirNodes]
       [fileNodes]
     </details>
diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean
index d96f2a9..beddf74 100644
--- a/DocGen4/ToHtmlFormat.lean
+++ b/DocGen4/ToHtmlFormat.lean
@@ -33,9 +33,9 @@ def attributesToString (attrs : Array (String × String)) :String :=
 
 -- TODO: Termination proof
 partial def toStringAux : Html → String
-| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>"
-| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>{child.toStringAux}</{tag}>"
-| element tag false attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"
+| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
+| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"
+| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"
 | element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"
 | text s => s