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