
   0 | module Text.Html.Node
   1 | 
   2 | import Data.String
   3 | import Text.Html.Attribute
   4 | import Text.Html.Event
   5 | import Web.Dom
   6 | 
   7 | %hide Web.Internal.DomTypes.Node
   8 | 
   9 | %default total
  10 | 
  11 | public export
  12 | data Node : (event : Type) -> Type where
  13 |   El    :  {0 ev : Type}
  14 |         -> (tag : String)
  15 |         -> List (Attribute ev)
  16 |         -> List (Node ev)
  17 |         -> Node ev
  18 | 
  19 |   Raw   : String -> Node ev
  20 | 
  21 |   Text  : String -> Node ev
  22 | 
  23 |   Empty : Node ev
  24 | 
  25 | public export %inline
  26 | FromString (Node ev) where
  27 |   fromString = Text
  28 | 
  29 | public export %inline
  30 | el :
  31 |      {tag : _}
  32 |   -> (0 et : ElementType tag e)
  33 |   -> List (Attribute ev)
  34 |   -> List (Node ev)
  35 |   -> Node ev
  36 | el _ = El tag
  37 | 
  38 | public export %inline
  39 | a : List (Attribute ev) -> List (Node ev) -> Node ev
  40 | a = el A
  41 | 
  42 | public export %inline
  43 | address : List (Attribute ev) -> List (Node ev) -> Node ev
  44 | address = el Address
  45 | 
  46 | public export %inline
  47 | area : List (Attribute ev) -> List (Node ev) -> Node ev
  48 | area = el Area
  49 | 
  50 | public export %inline
  51 | article : List (Attribute ev) -> List (Node ev) -> Node ev
  52 | article = el Article
  53 | 
  54 | public export %inline
  55 | audio : List (Attribute ev) -> List (Node ev) -> Node ev
  56 | audio = el Audio
  57 | 
  58 | public export %inline
  59 | base : List (Attribute ev) -> List (Node ev) -> Node ev
  60 | base = el Base
  61 | 
  62 | public export %inline
  63 | blockquote : List (Attribute ev) -> List (Node ev) -> Node ev
  64 | blockquote = el Blockquote
  65 | 
  66 | public export %inline
  67 | body : List (Attribute ev) -> List (Node ev) -> Node ev
  68 | body = el Body
  69 | 
  70 | public export %inline
  71 | br : List (Attribute ev) -> List (Node ev) -> Node ev
  72 | br = el Br
  73 | 
  74 | public export %inline
  75 | button : List (Attribute ev) -> List (Node ev) -> Node ev
  76 | button = el Button
  77 | 
  78 | public export %inline
  79 | canvas : List (Attribute ev) -> List (Node ev) -> Node ev
  80 | canvas = el Canvas
  81 | 
  82 | public export %inline
  83 | caption : List (Attribute ev) -> List (Node ev) -> Node ev
  84 | caption = el Caption
  85 | 
  86 | public export %inline
  87 | col : List (Attribute ev) -> List (Node ev) -> Node ev
  88 | col = el Col
  89 | 
  90 | public export %inline
  91 | colgroup : List (Attribute ev) -> List (Node ev) -> Node ev
  92 | colgroup = el Colgroup
  93 | 
  94 | public export %inline
  95 | data_ : List (Attribute ev) -> List (Node ev) -> Node ev
  96 | data_ = el Data
  97 | 
  98 | public export %inline
  99 | datalist : List (Attribute ev) -> List (Node ev) -> Node ev
 100 | datalist = el Datalist
 101 | 
 102 | public export %inline
 103 | del : List (Attribute ev) -> List (Node ev) -> Node ev
 104 | del = el Del
 105 | 
 106 | public export %inline
 107 | details : List (Attribute ev) -> List (Node ev) -> Node ev
 108 | details = el Details
 109 | 
 110 | public export %inline
 111 | dialog : List (Attribute ev) -> List (Node ev) -> Node ev
 112 | dialog = el Dialog
 113 | 
 114 | public export %inline
 115 | div : List (Attribute ev) -> List (Node ev) -> Node ev
 116 | div = el Div
 117 | 
 118 | public export %inline
 119 | dl : List (Attribute ev) -> List (Node ev) -> Node ev
 120 | dl = el Dl
 121 | 
 122 | public export %inline
 123 | embed : List (Attribute ev) -> List (Node ev) -> Node ev
 124 | embed = el Embed
 125 | 
 126 | public export %inline
 127 | fieldset : List (Attribute ev) -> List (Node ev) -> Node ev
 128 | fieldset = el FieldSet
 129 | 
 130 | public export %inline
 131 | footer : List (Attribute ev) -> List (Node ev) -> Node ev
 132 | footer = el Footer
 133 | 
 134 | public export %inline
 135 | form : List (Attribute ev) -> List (Node ev) -> Node ev
 136 | form = el Form
 137 | 
 138 | public export %inline
 139 | h1 : List (Attribute ev) -> List (Node ev) -> Node ev
 140 | h1 = el H1
 141 | 
 142 | public export %inline
 143 | h2 : List (Attribute ev) -> List (Node ev) -> Node ev
 144 | h2 = el H2
 145 | 
 146 | public export %inline
 147 | h3 : List (Attribute ev) -> List (Node ev) -> Node ev
 148 | h3 = el H3
 149 | 
 150 | public export %inline
 151 | h4 : List (Attribute ev) -> List (Node ev) -> Node ev
 152 | h4 = el H4
 153 | 
 154 | public export %inline
 155 | h5 : List (Attribute ev) -> List (Node ev) -> Node ev
 156 | h5 = el H5
 157 | 
 158 | public export %inline
 159 | h6 : List (Attribute ev) -> List (Node ev) -> Node ev
 160 | h6 = el H6
 161 | 
 162 | public export %inline
 163 | header : List (Attribute ev) -> List (Node ev) -> Node ev
 164 | header = el Header
 165 | 
 166 | public export %inline
 167 | hr : List (Attribute ev) -> List (Node ev) -> Node ev
 168 | hr = el HR
 169 | 
 170 | public export %inline
 171 | html : List (Attribute ev) -> List (Node ev) -> Node ev
 172 | html = el Html
 173 | 
 174 | public export %inline
 175 | iframe : List (Attribute ev) -> List (Node ev) -> Node ev
 176 | iframe = el IFrame
 177 | 
 178 | public export %inline
 179 | img : List (Attribute ev) -> List (Node ev) -> Node ev
 180 | img = el Img
 181 | 
 182 | public export %inline
 183 | input : List (Attribute ev) -> List (Node ev) -> Node ev
 184 | input = el Input
 185 | 
 186 | public export %inline
 187 | ins : List (Attribute ev) -> List (Node ev) -> Node ev
 188 | ins = el Ins
 189 | 
 190 | public export %inline
 191 | label : List (Attribute ev) -> List (Node ev) -> Node ev
 192 | label = el Label
 193 | 
 194 | public export %inline
 195 | legend : List (Attribute ev) -> List (Node ev) -> Node ev
 196 | legend = el Legend
 197 | 
 198 | public export %inline
 199 | li : List (Attribute ev) -> List (Node ev) -> Node ev
 200 | li = el Li
 201 | 
 202 | public export %inline
 203 | link : List (Attribute ev) -> List (Node ev) -> Node ev
 204 | link = el Link
 205 | 
 206 | public export %inline
 207 | map : List (Attribute ev) -> List (Node ev) -> Node ev
 208 | map = el Map
 209 | 
 210 | public export %inline
 211 | menu : List (Attribute ev) -> List (Node ev) -> Node ev
 212 | menu = el Menu
 213 | 
 214 | public export %inline
 215 | meta : List (Attribute ev) -> List (Node ev) -> Node ev
 216 | meta = el Meta
 217 | 
 218 | public export %inline
 219 | meter : List (Attribute ev) -> List (Node ev) -> Node ev
 220 | meter = el Meter
 221 | 
 222 | public export %inline
 223 | object : List (Attribute ev) -> List (Node ev) -> Node ev
 224 | object = el Object
 225 | 
 226 | public export %inline
 227 | ol : List (Attribute ev) -> List (Node ev) -> Node ev
 228 | ol = el Ol
 229 | 
 230 | public export %inline
 231 | optgroup : List (Attribute ev) -> List (Node ev) -> Node ev
 232 | optgroup = el OptGroup
 233 | 
 234 | public export %inline
 235 | option : List (Attribute ev) -> List (Node ev) -> Node ev
 236 | option = el Option
 237 | 
 238 | public export %inline
 239 | output : List (Attribute ev) -> List (Node ev) -> Node ev
 240 | output = el Output
 241 | 
 242 | public export %inline
 243 | p : List (Attribute ev) -> List (Node ev) -> Node ev
 244 | p = el P
 245 | 
 246 | public export %inline
 247 | param : List (Attribute ev) -> List (Node ev) -> Node ev
 248 | param = el Param
 249 | 
 250 | public export %inline
 251 | picture : List (Attribute ev) -> List (Node ev) -> Node ev
 252 | picture = el Picture
 253 | 
 254 | public export %inline
 255 | pre : List (Attribute ev) -> List (Node ev) -> Node ev
 256 | pre = el Pre
 257 | 
 258 | public export %inline
 259 | progress : List (Attribute ev) -> List (Node ev) -> Node ev
 260 | progress = el Progress
 261 | 
 262 | public export %inline
 263 | q : List (Attribute ev) -> List (Node ev) -> Node ev
 264 | q = el Q
 265 | 
 266 | public export %inline
 267 | script : List (Attribute ev) -> List (Node ev) -> Node ev
 268 | script = el Script
 269 | 
 270 | public export %inline
 271 | section : List (Attribute ev) -> List (Node ev) -> Node ev
 272 | section = el Section
 273 | 
 274 | public export %inline
 275 | select : List (Attribute ev) -> List (Node ev) -> Node ev
 276 | select = el Select
 277 | 
 278 | public export %inline
 279 | slot : List (Attribute ev) -> List (Node ev) -> Node ev
 280 | slot = el Slot
 281 | 
 282 | public export %inline
 283 | source : List (Attribute ev) -> List (Node ev) -> Node ev
 284 | source = el Source
 285 | 
 286 | public export %inline
 287 | span : List (Attribute ev) -> List (Node ev) -> Node ev
 288 | span = el Span
 289 | 
 290 | public export %inline
 291 | style : List (Attribute ev) -> List (Node ev) -> Node ev
 292 | style = el Style
 293 | 
 294 | public export %inline
 295 | table : List (Attribute ev) -> List (Node ev) -> Node ev
 296 | table = el Table
 297 | 
 298 | public export %inline
 299 | tbody : List (Attribute ev) -> List (Node ev) -> Node ev
 300 | tbody = el Tbody
 301 | 
 302 | public export %inline
 303 | td : List (Attribute ev) -> List (Node ev) -> Node ev
 304 | td = el Td
 305 | 
 306 | public export %inline
 307 | template : List (Attribute ev) -> List (Node ev) -> Node ev
 308 | template = el Template
 309 | 
 310 | public export %inline
 311 | textarea : List (Attribute ev) -> List (Node ev) -> Node ev
 312 | textarea = el TextArea
 313 | 
 314 | public export %inline
 315 | tfoot : List (Attribute ev) -> List (Node ev) -> Node ev
 316 | tfoot = el Tfoot
 317 | 
 318 | public export %inline
 319 | th : List (Attribute ev) -> List (Node ev) -> Node ev
 320 | th = el Th
 321 | 
 322 | public export %inline
 323 | thead : List (Attribute ev) -> List (Node ev) -> Node ev
 324 | thead = el Thead
 325 | 
 326 | public export %inline
 327 | time : List (Attribute ev) -> List (Node ev) -> Node ev
 328 | time = el Time
 329 | 
 330 | public export %inline
 331 | title : List (Attribute ev) -> List (Node ev) -> Node ev
 332 | title = el Title
 333 | 
 334 | public export %inline
 335 | tr : List (Attribute ev) -> List (Node ev) -> Node ev
 336 | tr = el Tr
 337 | 
 338 | public export %inline
 339 | track : List (Attribute ev) -> List (Node ev) -> Node ev
 340 | track = el Track
 341 | 
 342 | public export %inline
 343 | ul : List (Attribute ev) -> List (Node ev) -> Node ev
 344 | ul = el Ul
 345 | 
 346 | public export %inline
 347 | video : List (Attribute ev) -> List (Node ev) -> Node ev
 348 | video = el Video
 349 | 
 350 | --------------------------------------------------------------------------------
 351 | --          Rendering Html
 352 | --------------------------------------------------------------------------------
 353 | 
 354 | export
 355 | escape : String -> String
 356 | escape = fastConcat . map esc . unpack
 357 | 
 358 |   where
 359 |     esc : Char -> String
 360 |     esc '<'  = "&lt;"
 361 |     esc '>'  = "&gt;"
 362 |     esc '&'  = "&amp;"
 363 |     esc '"'  = "&quot;"
 364 |     esc '\'' = "&#x27"
 365 |     esc '\n' = "\n"
 366 |     esc '\r' = "\r"
 367 |     esc '\t' = "\t"
 368 |     esc c    = if c < ' ' then "" else singleton c
 369 | 
 370 | attrs : List (Attribute ev) -> String
 371 | attrs as = let s = displayAttributes as in if null s then "" else " " ++ s
 372 | 
 373 | export
 374 | render : Node ev -> String
 375 | render n = case n of
 376 |   Raw x         => x
 377 |   Text x        => escape x
 378 |   El tag as ns  => "<\{tag}\{attrs as}>\{go [<] ns}</\{tag}>"
 379 |   Empty         => ""
 380 | 
 381 |   where
 382 |     go : SnocList String -> List (Node ev) -> String
 383 |     go ss (n :: ns) = go (ss :< render n) ns
 384 |     go ss []        = concat $ ss <>> []
 385 | 
 386 | export
 387 | renderMany : List (Node ev) -> String
 388 | renderMany = fastConcat . map render
 389 |