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 =
"\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