diff --git a/SSG.ipkg b/SSG.ipkg index 3e8c0b2..0033da9 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -13,12 +13,14 @@ authors = "Nathan McCarty" -- langversion -- packages to add to search path -depends = eff +depends = structures + , eff -- modules to install modules = SSG.Parser.Core , SSG.Parser.Markdown , SSG.HTML + , SSG.HTML.ElementTypes -- main file (i.e. file to load at REPL) main = Main diff --git a/src/SSG/HTML.idr b/src/SSG/HTML.idr index 7ca024f..17f3322 100644 --- a/src/SSG/HTML.idr +++ b/src/SSG/HTML.idr @@ -1 +1,71 @@ module SSG.HTML + +import public SSG.HTML.ElementTypes + +import Data.String + +import Structures.Dependent.DList + +export infix 8 =$ + +public export +data Attribute : Type where + -- TODO: Add some structure here, maybe make `=$` a smart constructor + (=$) : (attribute, value : String) -> Attribute + +namespace Attribute + export + toString : Attribute -> String + toString (attribute =$ value) = + let value_cs = unpack value + in if any (== '\'') value_cs + then "\"\{value}\"" + else if any (== '"') value_cs || any (== ' ') value_cs + then "'\{value}'" + else value + +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 "" + ||| A void type tag, has attributes, no contents + Void : (type : String) -> {auto void_prf : IsVoid type} + -> (attributes : List Attribute) + -> Tag 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 + ||| 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 + +namespace Tag + viewIndented : (indent_level : Nat) -> Tag type -> String + viewIndented indent_level (Raw content) = + replicate (indent_level * 2) ' ' ++ content + viewIndented indent_level (Void type attributes) = + 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 (RawText type attributes content) = + ?viewIndented_rhs_3 + + view : Tag type -> String + view = viewIndented 0 + + render : Tag "html" -> String + render x = + "\n" ++ viewIndented 0 x diff --git a/src/SSG/HTML/ElementTypes.idr b/src/SSG/HTML/ElementTypes.idr new file mode 100644 index 0000000..e767ea5 --- /dev/null +++ b/src/SSG/HTML/ElementTypes.idr @@ -0,0 +1,98 @@ +module SSG.HTML.ElementTypes + +||| Proof that the element type identified by the given string is a void element +public export +data IsVoid : String -> Type where + IsArea : IsVoid "area" + IsBase : IsVoid "base" + IsBr : IsVoid "br" + IsCol : IsVoid "col" + IsImg : IsVoid "img" + IsInput : IsVoid "input" + IsLink : IsVoid "link" + IsMeta : IsVoid "meta" + IsParam : IsVoid "param" + IsSource : IsVoid "source" + IsTrack : IsVoid "track" + IsWbr : IsVoid "wbr" + +||| Proof that the element type identified by the given string is a raw text +||| element +public export +data IsRawText : String -> Type where + IsScript : IsRawText "script" + IsStyle : IsRawText "style" +||| Proof that the element type identified by the given string is an escapable +||| raw text element +public export +data IsEscapableRawText : String -> Type where + IsTextarea : IsEscapableRawText "textarea" + IsTitle : IsEscapableRawText "title" + +||| Proof that the element type idenitified by the given string is a normal +||| element +public export +data IsNormal : String -> Type where + -- Document element + IsHtml : IsNormal "html" + -- Sections + IsBody : IsNormal "body" + IsArticle : IsNormal "article" + IsSection : IsNormal "section" + IsNav : IsNormal "nav" + IsAside : IsNormal "aside" + IsH1 : IsNormal "h1" + IsH2 : IsNormal "h2" + IsH3 : IsNormal "h3" + IsH4 : IsNormal "h4" + IsH5 : IsNormal "h5" + IsH6 : IsNormal "h6" + IsHgroup : IsNormal "hgroup" + IsHeader : IsNormal "header" + IsFooter : IsNormal "footer" + IsAddress : IsNormal "address" + -- Grouping content + IsP : IsNormal "p" + IsHr : IsNormal "hr" + IsPre : IsNormal "pre" + IsBlockquote : IsNormal "blockquote" + IsOl : IsNormal "ol" + IsUl : IsNormal "ul" + IsMenu : IsNormal "menu" + IsLi : IsNormal "li" + IsDl : IsNormal "dl" + IsDt : IsNormal "dt" + IsDd : IsNormal "dd" + IsFigure : IsNormal "figure" + IsFigcaption : IsNormal "figcaption" + IsMain : IsNormal "main" + IsSearch : IsNormal "search" + IsDiv : IsNormal "div" + -- Text level semantics + IsA : IsNormal "a" + IsEm : IsNormal "em" + IsStrong : IsNormal "strong" + IsSmall : IsNormal "small" + IsS : IsNormal "s" + IsCite : IsNormal "cite" + IsQ : IsNormal "q" + IsDfn : IsNormal "dfn" + IsAbbr : IsNormal "abbr" + IsRuby : IsNormal "ruby" + IsRt : IsNormal "rt" + IsRp : IsNormal "rp" + IsData : IsNormal "data" + IsTime : IsNormal "time" + IsCode : IsNormal "code" + IsVar : IsNormal "var" + IsSamp : IsNormal "samp" + IsKbd : IsNormal "kbd" + IsSub : IsNormal "sub" + IsSup : IsNormal "sup" + IsI : IsNormal "i" + IsB : IsNormal "b" + IsU : IsNormal "u" + IsMark : IsNormal "mark" + IsBdi : IsNormal "bdi" + IsBdo : IsNormal "bdo" + IsSpan : IsNormal "span" diff --git a/todo.org b/todo.org new file mode 100644 index 0000000..f9056b9 --- /dev/null +++ b/todo.org @@ -0,0 +1,5 @@ +* HTML Handling +** 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=