From 0efbcd1f60596c0d0235fe0b224ebbdc1a9ce798 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 25 Dec 2021 14:04:35 +0100
Subject: [PATCH] feat: Newline free HTML formatting

Some of the HTML elements we are generating are newline sensitive
which requires the HTML to String formatter to optionally omit
additional newlines.
---
 DocGen4/Output/Navbar.lean |  4 ++--
 DocGen4/ToHtmlFormat.lean  | 15 ++++++++-------
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index c787279..6a2e07a 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -22,7 +22,7 @@ def moduleListFile (file : Name) : HtmlM Html := do
       #[("class", "nav_link")]
   | none => #[("class", "nav_link")]
   let nodes := #[<a href={s!"{←moduleNameToLink file}"}>{file.toString}</a>]
-  return Html.element "div" attributes nodes
+  return Html.element "div" false attributes nodes
 
 partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   let children := Array.mk (h.getChildren.toList.map Prod.snd)
@@ -40,7 +40,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   | none =>
       #[("class", "nav_sect"), ("data-path", moduleLink)]
   let nodes := #[<summary>{h.getName.toString}</summary>] ++ dirNodes ++ fileNodes
-  return Html.element "details" attributes nodes
+  return Html.element "details" false attributes nodes
 
 def moduleList : HtmlM (Array Html) := do
   let hierarchy := (←getResult).hierarchy
diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean
index 4d6110b..e0fbfaf 100644
--- a/DocGen4/ToHtmlFormat.lean
+++ b/DocGen4/ToHtmlFormat.lean
@@ -18,8 +18,8 @@ open Lean
 
 inductive Html where
   -- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson
-  -- element (tag : String) (attrs : Array HtmlAttribute) (children : Array Html)
-  | element : String → Array (String × String) → Array Html → Html
+  -- element (tag : String) (flatten : Bool) (attrs : Array HtmlAttribute) (children : Array Html)
+  | element : String → Bool → Array (String × String) → Array Html → Html
   | text : String → Html
   deriving Repr, BEq, Inhabited, FromJson, ToJson
 
@@ -33,9 +33,10 @@ def attributesToString (attrs : Array (String × String)) :String :=
 
 -- TODO: Termination proof
 partial def toStringAux : Html → String
-| element tag attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
-| element tag attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"
-| element tag attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"
+| 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
 
 def toString (html : Html) : String :=
@@ -83,7 +84,7 @@ macro_rules
       | `(jsxAttrVal| $s:strLit) => s
       | `(jsxAttrVal| { $t:term }) => t
       | _ => unreachable!
-    `(Html.element $(quote <| toString n.getId) #[ $[($ns, $vs)],* ] #[])
+    `(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)
@@ -99,7 +100,7 @@ macro_rules
         | `(jsxChild|$e:jsxElement) => `(#[$e:jsxElement])
         | _                         => unreachable!
       let tag := toString n.getId
-      `(Html.element $(quote tag) #[ $[($ns, $vs)],* ] (Array.foldl Array.append #[] #[ $[$cs],* ]))
+      `(Html.element $(quote tag) false #[ $[($ns, $vs)],* ] (Array.foldl Array.append #[] #[ $[$cs],* ]))
     else Macro.throwError ("expected </" ++ toString n.getId ++ ">")
 
 end Jsx