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

Round out basic html

Browse source
This commit is contained in:
Nathan McCarty 2025-02-18 23:07:30 -05:00
parent 33a4ad6dc8
commit 8098ed3c53
2 changed files with 45 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
src/SSG/HTML.idr
View file

@ -3,17 +3,20 @@ module SSG.HTML
import public SSG.HTML.ElementTypes import public SSG.HTML.ElementTypes
import Data.String import Data.String
import Decidable.Equality
import Structures.Dependent.DList import Structures.Dependent.DList
export infix 8 =$ export infix 8 =$
||| An attribute within an HTML tag
public export public export
data Attribute : Type where data Attribute : Type where
-- TODO: Add some structure here, maybe make `=$` a smart constructor -- TODO: Add some structure here, maybe make `=$` a smart constructor
(=$) : (attribute, value : String) -> Attribute (=$) : (attribute, value : String) -> Attribute
namespace Attribute namespace Attribute
||| Convert an attribute tag into a string suitable for rendering a tag with
export export
toString : Attribute -> String toString : Attribute -> String
toString (attribute =$ value) = toString (attribute =$ value) =
@ -24,48 +27,68 @@ namespace Attribute
then "'\{value}'" then "'\{value}'"
else value else value
||| An element in an HTML document, indexed by the tag type.
|||
||| Raw text has a tag type of `""`
public export public export
data Tag : String -> Type where data Html : String -> Type where
-- TODO: Find a way to move this out of tag ||| Textual content outside of a tag
||| Raw text, represented as a tag for compatibility Text : (content : String)
Raw : (content : String) -> Html ""
-> Tag ""
||| A void type tag, has attributes, no contents ||| A void type tag, has attributes, no contents
Void : (type : String) -> {auto void_prf : IsVoid type} Void : (type : String) -> {auto void_prf : IsVoid type}
-> (attributes : List Attribute) -> (attributes : List Attribute)
-> Tag type -> Html type
||| A normal type tag, has attributes, and contents ||| A normal type tag, has attributes, and contents
Normal : (type : String) -> {auto normal_prf : IsNormal type} Normal : (type : String) -> {auto normal_prf : IsNormal type}
-> (attributes : List Attribute) -> (attributes : List Attribute)
-- TODO: Erase content_types -> {content_types : _} -> (contents : DList _ Html content_types)
-> {content_types : _} -> (contents : DList _ Tag content_types) -> Html type
-> Tag type
||| A raw text or an escapable raw text element ||| A raw text or an escapable raw text element
RawText : (type : String) RawText : (type : String)
-> {auto raw_prf : Either (IsRawText type) (IsEscapableRawText type)} -> {auto raw_prf : Either (IsRawText type) (IsEscapableRawText type)}
-> (attributes : List Attribute) -> (attributes : List Attribute)
-> (content : String) -> (content : String)
-> Tag type -> Html type
namespace Tag namespace Html
viewIndented : (indent_level : Nat) -> Tag type -> String ||| Convert to a "pretty printed" string containing the html, starting at the
viewIndented indent_level (Raw content) = ||| specified indentation level
viewIndented : (indent_level : Nat) -> Html type -> String
viewIndented indent_level (Text content) =
replicate (indent_level * 2) ' ' ++ content replicate (indent_level * 2) ' ' ++ content
viewIndented indent_level (Void type attributes) = viewIndented indent_level (Void type attributes) =
let indent = replicate (indent_level * 2) ' ' let indent = replicate (indent_level * 2) ' ' in
in if length attributes > 0 if length attributes > 0
then then
let attrs = joinBy " " $ map toString attributes let attrs = joinBy " " $ map toString attributes
in "<\{type} \{attrs} />" in "<\{type} \{attrs} />"
else "<\{type} />" else "<\{type} />"
viewIndented indent_level (Normal type attributes contents) = viewIndented indent_level (Normal type attributes {content_types} contents) =
?viewIndented_rhs_2 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 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 view = viewIndented 0
render : Tag "html" -> String ||| Render a top level html document, including the doctype tag
render : Html "html" -> String
render x = render x =
"<!DOCTYPE HTML>\n" ++ viewIndented 0 x "<!DOCTYPE HTML>\n" ++ viewIndented 0 x

3
todo.org
View file

@ -2,4 +2,5 @@
** TODO Special handling for =pre= in =view= ** TODO Special handling for =pre= in =view=
** TODO Smart spec compliance for =attribute= ** 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. 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