From dc3c49cdf6759bb24ef0ea06adb785c15abe78e2 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Tue, 18 Feb 2025 23:40:53 -0500
Subject: [PATCH] Working html generation example

---
 examples/examples.ipkg        | 48 +++++++++++++++++++++++++++++++++++
 examples/src/HelloWorld.idr   | 19 ++++++++++++++
 pack.toml                     |  7 ++++-
 src/SSG/HTML.idr              | 34 +++++++++++++++++--------
 src/SSG/HTML/ElementTypes.idr |  1 +
 5 files changed, 97 insertions(+), 12 deletions(-)
 create mode 100644 examples/examples.ipkg
 create mode 100644 examples/src/HelloWorld.idr

diff --git a/examples/examples.ipkg b/examples/examples.ipkg
new file mode 100644
index 0000000..a8cdedb
--- /dev/null
+++ b/examples/examples.ipkg
@@ -0,0 +1,48 @@
+package ssg-examples
+version = 0.1.0
+authors = "Nathan McCarty"
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+-- langversion
+
+-- packages to add to search path
+depends = SSG
+        , structures
+
+-- modules to install
+modules = HelloWorld
+
+-- main file (i.e. file to load at REPL)
+-- main = Main
+
+-- name of executable
+-- executable = "SSG-test"
+-- opts =
+sourcedir = "src"
+-- builddir =
+-- outputdir =
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =
diff --git a/examples/src/HelloWorld.idr b/examples/src/HelloWorld.idr
new file mode 100644
index 0000000..7f51a83
--- /dev/null
+++ b/examples/src/HelloWorld.idr
@@ -0,0 +1,19 @@
+module HelloWorld
+
+import SSG.HTML
+
+import Structures.Dependent.DList
+
+helloWorld : Html "html"
+helloWorld =
+  Normal "html" ["lang" =$ "en"] [
+    Normal "head" [] [
+      RawText "title" [] "Example"
+    ],
+    Normal "body" [] [
+      Normal "p" [] [Text "Hello World!"]
+    ]
+  ]
+
+main : IO ()
+main = putStr $ render helloWorld
diff --git a/pack.toml b/pack.toml
index 44fed03..eed6e77 100644
--- a/pack.toml
+++ b/pack.toml
@@ -7,4 +7,9 @@ test = "test/test.ipkg"
 [custom.all.SSG-test]
 type = "local"
 path = "test"
-ipkg = "test.ipkg"
\ No newline at end of file
+ipkg = "test.ipkg"
+
+[custom.all.ssg-examples]
+type = "local"
+path = "examples"
+ipkg = "examples.ipkg"
diff --git a/src/SSG/HTML.idr b/src/SSG/HTML.idr
index 7780842..c96905f 100644
--- a/src/SSG/HTML.idr
+++ b/src/SSG/HTML.idr
@@ -5,7 +5,7 @@ import public SSG.HTML.ElementTypes
 import Data.String
 import Decidable.Equality
 
-import Structures.Dependent.DList
+import public Structures.Dependent.DList
 
 export infix 8 =$
 
@@ -22,10 +22,10 @@ namespace Attribute
   toString (attribute =$ value) =
     let value_cs = unpack value
     in if any (== '\'') value_cs
-      then "\"\{value}\""
+      then "\{attribute}=\"\{value}\""
       else if any (== '"') value_cs || any (== ' ') value_cs
-        then "'\{value}'"
-        else value
+        then "\{attribute}='\{value}'"
+        else "\{attribute}=\{value}"
 
 ||| An element in an HTML document, indexed by the tag type.
 |||
@@ -54,6 +54,7 @@ data Html : String -> Type where
 namespace Html
   ||| Convert to a "pretty printed" string containing the html, starting at the
   ||| specified indentation level
+  export
   viewIndented : (indent_level : Nat) -> Html type -> String
   viewIndented indent_level (Text content) =
     replicate (indent_level * 2) ' ' ++ content
@@ -68,27 +69,38 @@ namespace Html
     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
+    case decEq [""] content_types of
+      Yes prf => assert_total $ -- BUG Compiler Bug ???
+        let [Text content] : DList _ Html [""] = rewrite prf in contents
+        in if length attributes > 0
+          then
+            let attrs = joinBy " " $ map toString attributes
+            in "\{indent}<\{type} \{attrs}>\{content}</\{type}>"
+          else "\{indent}<\{type}>\{content}</\{type}>"
       No contra =>
-        let start = "\{indent}<\{type}>\n"
-            end = "\{indent}</\{type}>\n"
+        let end = "\n\{indent}</\{type}>"
             inner = joinBy "\n" $
                       dMap (\_, x => viewIndented (S indent_level) x) contents
-        in start ++ end ++ inner
+        in if length attributes > 0
+          then
+            let attrs = joinBy " " $ map toString attributes
+            in "\{indent}<\{type} \{attrs}>\n" ++ inner ++ end
+          else "\{indent}<\{type}>\n" ++ inner ++ end
   viewIndented indent_level (RawText type attributes content) =
     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}>"
+        in "\{indent}<\{type} \{attrs}>\{content}</\{type}>"
+      else "\{indent}<\{type}>\{content}</\{type}>"
 
   ||| Convert to a "pretty printed" string containing the html
+  export
   view : Html type -> String
   view = viewIndented 0
 
   ||| Render a top level html document, including the doctype tag
+  export
   render : Html "html" -> String
   render x =
     "<!DOCTYPE HTML>\n" ++ viewIndented 0 x
diff --git a/src/SSG/HTML/ElementTypes.idr b/src/SSG/HTML/ElementTypes.idr
index e767ea5..eaf5bb7 100644
--- a/src/SSG/HTML/ElementTypes.idr
+++ b/src/SSG/HTML/ElementTypes.idr
@@ -36,6 +36,7 @@ data IsNormal : String -> Type where
   -- Document element
   IsHtml : IsNormal "html"
   -- Sections
+  IsHead : IsNormal "head"
   IsBody : IsNormal "body"
   IsArticle : IsNormal "article"
   IsSection : IsNormal "section"