From 8098ed3c53b3dc4e3f2d86b5e42bcdc1461b649f Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Tue, 18 Feb 2025 23:07:30 -0500
Subject: [PATCH] Round out basic html

---
 src/SSG/HTML.idr | 63 +++++++++++++++++++++++++++++++++---------------
 todo.org         |  3 ++-
 2 files changed, 45 insertions(+), 21 deletions(-)

diff --git a/src/SSG/HTML.idr b/src/SSG/HTML.idr
index 17f3322..7780842 100644
--- a/src/SSG/HTML.idr
+++ b/src/SSG/HTML.idr
@@ -3,17 +3,20 @@ module SSG.HTML
 import public SSG.HTML.ElementTypes
 
 import Data.String
+import Decidable.Equality
 
 import Structures.Dependent.DList
 
 export infix 8 =$
 
+||| An attribute within an HTML tag
 public export
 data Attribute : Type where
   -- TODO: Add some structure here, maybe make `=$` a smart constructor
   (=$) : (attribute, value : String) -> Attribute
 
 namespace Attribute
+  ||| Convert an attribute tag into a string suitable for rendering a tag with
   export
   toString : Attribute -> String
   toString (attribute =$ value) =
@@ -24,48 +27,68 @@ namespace Attribute
         then "'\{value}'"
         else value
 
+||| An element in an HTML document, indexed by the tag type.
+|||
+||| Raw text has a tag type of `""`
 public export
-data Tag : String -> Type where
-  -- TODO: Find a way to move this out of tag
-  ||| Raw text, represented as a tag for compatibility
-  Raw : (content : String)
-    -> Tag ""
+data Html : String -> Type where
+  ||| Textual content outside of a tag
+  Text : (content : String)
+    -> Html ""
   ||| A void type tag, has attributes, no contents
   Void : (type : String) -> {auto void_prf : IsVoid type}
     -> (attributes : List Attribute)
-    -> Tag type
+    -> Html type
   ||| A normal type tag, has attributes, and contents
   Normal : (type : String) -> {auto normal_prf : IsNormal type}
     -> (attributes : List Attribute)
-    -- TODO: Erase content_types
-    -> {content_types : _} -> (contents : DList _ Tag content_types)
-    -> Tag type
+    -> {content_types : _} -> (contents : DList _ Html content_types)
+    -> Html type
   ||| A raw text or an escapable raw text element
   RawText : (type : String)
     -> {auto raw_prf : Either (IsRawText type) (IsEscapableRawText type)}
     -> (attributes : List Attribute)
     -> (content : String)
-    -> Tag type
+    -> Html type
 
-namespace Tag
-  viewIndented : (indent_level : Nat) -> Tag type -> String
-  viewIndented indent_level (Raw content) =
+namespace Html
+  ||| Convert to a "pretty printed" string containing the html, starting at the
+  ||| specified indentation level
+  viewIndented : (indent_level : Nat) -> Html type -> String
+  viewIndented indent_level (Text content) =
     replicate (indent_level * 2) ' ' ++ content
   viewIndented indent_level (Void type attributes) =
-    let indent = replicate (indent_level * 2) ' '
-    in if length attributes > 0
+    let indent = replicate (indent_level * 2) ' ' in
+    if length attributes > 0
       then
         let attrs = joinBy " " $ map toString attributes
         in "<\{type} \{attrs} />"
       else "<\{type} />"
-  viewIndented indent_level (Normal type attributes contents) =
-    ?viewIndented_rhs_2
+  viewIndented indent_level (Normal type attributes {content_types} contents) =
+    let indent = replicate (indent_level * 2) ' ' in
+    -- Special handling if the tag contains exactly one `Text` element, we won't
+    -- do any newlines between the tag and its contents in that case
+    case decEq content_types [""] of
+      Yes prf => ?viewIndented_rhs_4
+      No contra =>
+        let start = "\{indent}<\{type}>\n"
+            end = "\{indent}</\{type}>\n"
+            inner = joinBy "\n" $
+                      dMap (\_, x => viewIndented (S indent_level) x) contents
+        in start ++ end ++ inner
   viewIndented indent_level (RawText type attributes content) =
-    ?viewIndented_rhs_3
+    let indent = replicate (indent_level * 2) ' ' in
+    if length attributes > 0
+      then
+        let attrs = joinBy " " $ map toString attributes
+        in "<\{type} \{attrs}>\{content}</\{type}>"
+      else "<\{type}>\{content}</\{type}>"
 
-  view : Tag type -> String
+  ||| Convert to a "pretty printed" string containing the html
+  view : Html type -> String
   view = viewIndented 0
 
-  render : Tag "html" -> String
+  ||| Render a top level html document, including the doctype tag
+  render : Html "html" -> String
   render x =
     "<!DOCTYPE HTML>\n" ++ viewIndented 0 x
diff --git a/todo.org b/todo.org
index f9056b9..cda0ed9 100644
--- a/todo.org
+++ b/todo.org
@@ -2,4 +2,5 @@
 ** TODO Special handling for =pre= in =view=
 ** TODO Smart spec compliance for =attribute=
 Probably want to refine the attribute and value strings, and be smarter about how we choose to quote the value string.
-** TODO Move =Raw= out of =Tag=
+** NO Move =Raw= out of =Tag=
+Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make sense