From 135b8782339480fba3c00432a07c193c7b0cf063 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Thu, 27 Feb 2025 04:23:25 -0500
Subject: [PATCH] HTML rendering

---
 SSG.ipkg                |  1 +
 src/SSG/Djot.idr        |  4 ++++
 src/SSG/Djot/Render.idr | 37 +++++++++++++++++++++++++++++++++++++
 todo.org                |  1 +
 4 files changed, 43 insertions(+)
 create mode 100644 src/SSG/Djot/Render.idr

diff --git a/SSG.ipkg b/SSG.ipkg
index 2a04ca2..f462141 100644
--- a/SSG.ipkg
+++ b/SSG.ipkg
@@ -29,6 +29,7 @@ modules = SSG.HTML
         , SSG.Djot.Lines
         , SSG.Djot.Block
         , SSG.Djot.Inline
+        , SSG.Djot.Render
 
 -- main file (i.e. file to load at REPL)
 main = Main
diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr
index 584fa6a..0fb4599 100644
--- a/src/SSG/Djot.idr
+++ b/src/SSG/Djot.idr
@@ -1 +1,5 @@
 module SSG.Djot
+
+import public SSG.Djot.Inline
+import public SSG.Djot.Block
+import public SSG.Djot.Render
diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr
new file mode 100644
index 0000000..73cf01b
--- /dev/null
+++ b/src/SSG/Djot/Render.idr
@@ -0,0 +1,37 @@
+||| Render Djot to HTML
+module SSG.Djot.Render
+
+import SSG.HTML
+import SSG.Djot.Inline
+import SSG.Djot.Block
+
+||| Render a single inline element as HTML
+export
+renderInline : Inline -> (t ** Html t)
+-- FIXME: escape text
+renderInline (Text text) = (_ ** Text text)
+
+||| Render a list of inline elments to html
+export
+renderInlines : List Inline -> (types ** DList _ Html types)
+renderInlines xs = fromList $ map renderInline xs
+
+||| Render a single block element as HTML
+export
+renderBlock : Block t -> (t ** Html t)
+
+||| Render a list of block level elements to html
+export
+renderBlocks : {types: _} -> DList _ Block types -> (types' ** DList _ Html types')
+
+renderBlock (Paragraph content) =
+  (_ ** Normal "p" []  (snd (renderInlines content)))
+
+renderBlocks xs = dMap' (\_, x => renderBlock x) xs
+
+||| Render a complete html document from a list of block level elements
+renderDocument : {types : _} -> DList _ Block types -> Html "html"
+renderDocument xs =
+  Normal "html" ["lang" =$ "en"] [
+    Normal "body" [] (snd (renderBlocks xs))
+  ]
diff --git a/todo.org b/todo.org
index e3c77c7..ce5e9de 100644
--- a/todo.org
+++ b/todo.org
@@ -3,6 +3,7 @@
 ** 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 Don't generate any further indent once we are already inside a =p=
+** TODO Text escaping function
 ** NO Move =Raw= out of =Tag=
 Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make sense
 * Parser Core