HTML rendering

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

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

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))
+  ]

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