Merge pull request #83 from claudio-etterli/asideElement

Adding the 'aside' element
stefan-hoeck · Oct 10, 2024 · aa13b5c · aa13b5c
2 parents edc345e + def2bf5
commit aa13b5c
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/src/Text/HTML/Node.idr b/src/Text/HTML/Node.idr
@@ -78,6 +78,10 @@ export %inline
 article : List (Attribute Article ev) -> List (Node ev) -> Node ev
 article = El _
 
+export %inline
+aside : List (Attribute Aside ev) -> List (Node ev) -> Node ev
+aside = El _
+
 export %inline
 audio : List (Attribute Audio ev) -> List (Node ev) -> Node ev
 audio = El _

diff --git a/src/Text/HTML/Tag.idr b/src/Text/HTML/Tag.idr
@@ -12,6 +12,7 @@ data HTMLTag : (tag : String) -> Type where
  Address : HTMLTag "address"
  Area : HTMLTag "area"
  Article : HTMLTag "article"
+ Aside : HTMLTag "aside"
  Audio : HTMLTag "audio"
  Base : HTMLTag "base"
  Blockquote : HTMLTag "blockquote"