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

Working html generation example

Browse source
This commit is contained in:
Nathan McCarty 2025-02-18 23:40:53 -05:00
parent 8098ed3c53
commit dc3c49cdf6
5 changed files with 97 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/SSG/HTML.idr
View file

@ -5,7 +5,7 @@ import public SSG.HTML.ElementTypes
import Data.String
import Decidable.Equality
import Structures.Dependent.DList
import public Structures.Dependent.DList
export infix 8 =$
@ -22,10 +22,10 @@ namespace Attribute
toString (attribute =$ value) =
let value_cs = unpack value
in if any (== '\'') value_cs
then "\"\{value}\""
then "\{attribute}=\"\{value}\""
else if any (== '"') value_cs || any (== ' ') value_cs
then "'\{value}'"
else value
then "\{attribute}='\{value}'"
else "\{attribute}=\{value}"
||| An element in an HTML document, indexed by the tag type.
|||
@ -54,6 +54,7 @@ data Html : String -> Type where
namespace Html
||| Convert to a "pretty printed" string containing the html, starting at the
||| specified indentation level
export
viewIndented : (indent_level : Nat) -> Html type -> String
viewIndented indent_level (Text content) =
replicate (indent_level * 2) ' ' ++ content
@ -68,27 +69,38 @@ namespace Html
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
case decEq [""] content_types of
Yes prf => assert_total $ -- BUG Compiler Bug ???
let [Text content] : DList _ Html [""] = rewrite prf in contents
in if length attributes > 0
then
let attrs = joinBy " " $ map toString attributes
in "\{indent}<\{type} \{attrs}>\{content}</\{type}>"
else "\{indent}<\{type}>\{content}</\{type}>"
No contra =>
let start = "\{indent}<\{type}>\n"
end = "\{indent}</\{type}>\n"
let end = "\n\{indent}</\{type}>"
inner = joinBy "\n" $
dMap (\_, x => viewIndented (S indent_level) x) contents
in start ++ end ++ inner
in if length attributes > 0
then
let attrs = joinBy " " $ map toString attributes
in "\{indent}<\{type} \{attrs}>\n" ++ inner ++ end
else "\{indent}<\{type}>\n" ++ inner ++ end
viewIndented indent_level (RawText type attributes content) =
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}>"
in "\{indent}<\{type} \{attrs}>\{content}</\{type}>"
else "\{indent}<\{type}>\{content}</\{type}>"
||| Convert to a "pretty printed" string containing the html
export
view : Html type -> String
view = viewIndented 0
||| Render a top level html document, including the doctype tag
export
render : Html "html" -> String
render x =
"<!DOCTYPE HTML>\n" ++ viewIndented 0 x

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

@ -36,6 +36,7 @@ data IsNormal : String -> Type where
-- Document element
IsHtml : IsNormal "html"
-- Sections
IsHead : IsNormal "head"
IsBody : IsNormal "body"
IsArticle : IsNormal "article"
IsSection : IsNormal "section"