diff --git a/examples/src/HelloWorld.idr b/examples/src/HelloWorld.idr index 7f51a83..bd272ba 100644 --- a/examples/src/HelloWorld.idr +++ b/examples/src/HelloWorld.idr @@ -6,12 +6,12 @@ import Structures.Dependent.DList helloWorld : Html "html" helloWorld = - Normal "html" ["lang" =$ "en"] [ - Normal "head" [] [ - RawText "title" [] "Example" + tag "html" ["lang" =$ "en"] [ + tag "head" [] [ + tag "title" [] "Example" ], - Normal "body" [] [ - Normal "p" [] [Text "Hello World!"] + tag "body" [] [ + tag "p" [] [Text "Hello World!"] ] ] diff --git a/src/SSG/HTML.idr b/src/SSG/HTML.idr index c96905f..91c07f3 100644 --- a/src/SSG/HTML.idr +++ b/src/SSG/HTML.idr @@ -104,3 +104,29 @@ namespace Html render : Html "html" -> String render x = "\n" ++ viewIndented 0 x + + ||| Cacluate the type signature of the `tag` function + public export + TagType : IsValidTag type -> Type + TagType (PVoid type) = + (attributes : List Attribute) -> Html type + TagType (PRawText type) = + (attributes : List Attribute) -> (content : String) -> Html type + TagType (PEscapableRawText type) = + (attributes : List Attribute) -> (content : String) -> Html type + TagType (PNormal type) = + (attributes : List Attribute) + -> {content_types : _} -> (contents : DList _ Html content_types) + -> Html type + + public export + TagType' : (type : String) -> {auto prf : IsValidTag type} -> Type + TagType' type {prf} = TagType prf + + ||| Smart constructor for tags + public export + tag : (type : String) -> {auto prf : IsValidTag type} -> TagType prf + tag type {prf = (PVoid type)} = Void type + tag type {prf = (PRawText type)} = RawText type + tag type {prf = (PEscapableRawText type)} = RawText type + tag type {prf = (PNormal type)} = Normal type diff --git a/src/SSG/HTML/ElementTypes.idr b/src/SSG/HTML/ElementTypes.idr index eaf5bb7..c554a5d 100644 --- a/src/SSG/HTML/ElementTypes.idr +++ b/src/SSG/HTML/ElementTypes.idr @@ -97,3 +97,12 @@ data IsNormal : String -> Type where IsBdi : IsNormal "bdi" IsBdo : IsNormal "bdo" IsSpan : IsNormal "span" + +||| A proof that a string is a valid tag type +public export +data IsValidTag : String -> Type where + PVoid : (type : String) -> {auto prf : IsVoid type} -> IsValidTag type + PRawText : (type : String) -> {auto prf : IsRawText type} -> IsValidTag type + PEscapableRawText : (type : String) -> {auto prf : IsEscapableRawText type} + -> IsValidTag type + PNormal : (type : String) -> {auto prf : IsNormal type} -> IsValidTag type