Idris/ssg
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Non-working tag smart constructor

Browse source
This commit is contained in:
Nathan McCarty 2025-02-19 00:34:00 -05:00
parent dc3c49cdf6
commit 2929bceaa1
3 changed files with 40 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
examples/src/HelloWorld.idr
View file

@ -6,12 +6,12 @@ import Structures.Dependent.DList
helloWorld : Html "html" helloWorld : Html "html"
helloWorld = helloWorld =
Normal "html" ["lang" =$ "en"] [ tag "html" ["lang" =$ "en"] [
Normal "head" [] [ tag "head" [] [
RawText "title" [] "Example" tag "title" [] "Example"
], ],
Normal "body" [] [ tag "body" [] [
Normal "p" [] [Text "Hello World!"] tag "p" [] [Text "Hello World!"]
] ]
] ]

26
src/SSG/HTML.idr
View file

@ -104,3 +104,29 @@ namespace Html
render : Html "html" -> String render : Html "html" -> String
render x = render x =
"<!DOCTYPE HTML>\n" ++ viewIndented 0 x "<!DOCTYPE HTML>\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

9
src/SSG/HTML/ElementTypes.idr
View file

@ -97,3 +97,12 @@ data IsNormal : String -> Type where
IsBdi : IsNormal "bdi" IsBdi : IsNormal "bdi"
IsBdo : IsNormal "bdo" IsBdo : IsNormal "bdo"
IsSpan : IsNormal "span" 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