
   0 | module Web.Dom
   1 | 
   2 | import JS
   3 | import public Web.Internal.Types
   4 | import public Web.Raw.Dom as Dom
   5 | 
   6 | %default total
   7 | 
   8 | --------------------------------------------------------------------------------
   9 | --          Main entry points
  10 | --------------------------------------------------------------------------------
  11 | 
  12 | %foreign "browser:lambda:()=>window"
  13 | prim__window : PrimIO Window
  14 | 
  15 | %foreign "browser:lambda:()=>document"
  16 | prim__document : PrimIO Document
  17 | 
  18 | export
  19 | window : JSIO Window
  20 | window = primJS prim__window
  21 | 
  22 | export
  23 | document : JSIO Document
  24 | document = primJS prim__document
  25 | 
  26 | export
  27 | body : JSIO HTMLElement
  28 | body = unMaybe "Web.Dom.body" $ document >>= to body
  29 | 
  30 | --------------------------------------------------------------------------------
  31 | --          Aliases
  32 | --------------------------------------------------------------------------------
  33 | 
  34 | namespace Alias
  35 |   public export
  36 |   0 Anchor : Type
  37 |   Anchor = HTMLAnchorElement
  38 | 
  39 |   public export
  40 |   0 Area : Type
  41 |   Area = HTMLAreaElement
  42 | 
  43 |   public export
  44 |   0 Audio : Type
  45 |   Audio = HTMLAudioElement
  46 | 
  47 |   public export
  48 |   0 BR : Type
  49 |   BR = HTMLBRElement
  50 | 
  51 |   public export
  52 |   0 Base : Type
  53 |   Base = HTMLBaseElement
  54 | 
  55 |   public export
  56 |   0 Body : Type
  57 |   Body = HTMLBodyElement
  58 | 
  59 |   public export
  60 |   0 Button : Type
  61 |   Button = HTMLButtonElement
  62 | 
  63 |   public export
  64 |   0 Canvas : Type
  65 |   Canvas = HTMLCanvasElement
  66 | 
  67 |   public export
  68 |   0 DList : Type
  69 |   DList = HTMLDListElement
  70 | 
  71 |   public export
  72 |   0 Data : Type
  73 |   Data = HTMLDataElement
  74 | 
  75 |   public export
  76 |   0 DataList : Type
  77 |   DataList = HTMLDataListElement
  78 | 
  79 |   public export
  80 |   0 Details : Type
  81 |   Details = HTMLDetailsElement
  82 | 
  83 |   public export
  84 |   0 Dialog : Type
  85 |   Dialog = HTMLDialogElement
  86 | 
  87 |   public export
  88 |   0 Div : Type
  89 |   Div = HTMLDivElement
  90 | 
  91 |   public export
  92 |   0 Embed : Type
  93 |   Embed = HTMLEmbedElement
  94 | 
  95 |   public export
  96 |   0 FieldSet : Type
  97 |   FieldSet = HTMLFieldSetElement
  98 | 
  99 |   public export
 100 |   0 Form : Type
 101 |   Form = HTMLFormElement
 102 | 
 103 |   public export
 104 |   0 HR : Type
 105 |   HR = HTMLHRElement
 106 | 
 107 |   public export
 108 |   0 Heading : Type
 109 |   Heading = HTMLHeadingElement
 110 | 
 111 |   public export
 112 |   0 Html : Type
 113 |   Html = HTMLHtmlElement
 114 | 
 115 |   public export
 116 |   0 IFrame : Type
 117 |   IFrame = HTMLIFrameElement
 118 | 
 119 |   public export
 120 |   0 Image : Type
 121 |   Image = HTMLImageElement
 122 | 
 123 |   public export
 124 |   0 Input : Type
 125 |   Input = HTMLInputElement
 126 | 
 127 |   public export
 128 |   0 LI : Type
 129 |   LI = HTMLLIElement
 130 | 
 131 |   public export
 132 |   0 Label : Type
 133 |   Label = HTMLLabelElement
 134 | 
 135 |   public export
 136 |   0 Legend : Type
 137 |   Legend = HTMLLegendElement
 138 | 
 139 |   public export
 140 |   0 Link : Type
 141 |   Link = HTMLLinkElement
 142 | 
 143 |   public export
 144 |   0 Map : Type
 145 |   Map = HTMLMapElement
 146 | 
 147 |   public export
 148 |   0 Menu : Type
 149 |   Menu = HTMLMenuElement
 150 | 
 151 |   public export
 152 |   0 Meta : Type
 153 |   Meta = HTMLMetaElement
 154 | 
 155 |   public export
 156 |   0 Meter : Type
 157 |   Meter = HTMLMeterElement
 158 | 
 159 |   public export
 160 |   0 Mod : Type
 161 |   Mod = HTMLModElement
 162 | 
 163 |   public export
 164 |   0 OList : Type
 165 |   OList = HTMLOListElement
 166 | 
 167 |   public export
 168 |   0 Object : Type
 169 |   Object = HTMLObjectElement
 170 | 
 171 |   public export
 172 |   0 OptGroup : Type
 173 |   OptGroup = HTMLOptGroupElement
 174 | 
 175 |   public export
 176 |   0 Option : Type
 177 |   Option = HTMLOptionElement
 178 | 
 179 |   public export
 180 |   0 Output : Type
 181 |   Output = HTMLOutputElement
 182 | 
 183 |   public export
 184 |   0 Paragraph : Type
 185 |   Paragraph = HTMLParagraphElement
 186 | 
 187 |   public export
 188 |   0 Param : Type
 189 |   Param = HTMLParamElement
 190 | 
 191 |   public export
 192 |   0 Picture : Type
 193 |   Picture = HTMLPictureElement
 194 | 
 195 |   public export
 196 |   0 Pre : Type
 197 |   Pre = HTMLPreElement
 198 | 
 199 |   public export
 200 |   0 Progress : Type
 201 |   Progress = HTMLProgressElement
 202 | 
 203 |   public export
 204 |   0 Quote : Type
 205 |   Quote = HTMLQuoteElement
 206 | 
 207 |   public export
 208 |   0 Script : Type
 209 |   Script = HTMLScriptElement
 210 | 
 211 |   public export
 212 |   0 Select : Type
 213 |   Select = HTMLSelectElement
 214 | 
 215 |   public export
 216 |   0 Slot : Type
 217 |   Slot = HTMLSlotElement
 218 | 
 219 |   public export
 220 |   0 Source : Type
 221 |   Source = HTMLSourceElement
 222 | 
 223 |   public export
 224 |   0 Span : Type
 225 |   Span = HTMLSpanElement
 226 | 
 227 |   public export
 228 |   0 Style : Type
 229 |   Style = HTMLStyleElement
 230 | 
 231 |   public export
 232 |   0 TableCaption : Type
 233 |   TableCaption = HTMLTableCaptionElement
 234 | 
 235 |   public export
 236 |   0 TableCell : Type
 237 |   TableCell = HTMLTableCellElement
 238 | 
 239 |   public export
 240 |   0 TableCol : Type
 241 |   TableCol = HTMLTableColElement
 242 | 
 243 |   public export
 244 |   0 Table : Type
 245 |   Table = HTMLTableElement
 246 | 
 247 |   public export
 248 |   0 TableRow : Type
 249 |   TableRow = HTMLTableRowElement
 250 | 
 251 |   public export
 252 |   0 TableSection : Type
 253 |   TableSection = HTMLTableSectionElement
 254 | 
 255 |   public export
 256 |   0 Template : Type
 257 |   Template = HTMLTemplateElement
 258 | 
 259 |   public export
 260 |   0 TextArea : Type
 261 |   TextArea = HTMLTextAreaElement
 262 | 
 263 |   public export
 264 |   0 Time : Type
 265 |   Time = HTMLTimeElement
 266 | 
 267 |   public export
 268 |   0 Title : Type
 269 |   Title = HTMLTitleElement
 270 | 
 271 |   public export
 272 |   0 Track : Type
 273 |   Track = HTMLTrackElement
 274 | 
 275 |   public export
 276 |   0 UList : Type
 277 |   UList = HTMLUListElement
 278 | 
 279 |   public export
 280 |   0 Video : Type
 281 |   Video = HTMLVideoElement
 282 | 
 283 | --------------------------------------------------------------------------------
 284 | --          Elements
 285 | --------------------------------------------------------------------------------
 286 | 
 287 | ||| HTML Element Tags linking tag names with HTML element types
 288 | |||
 289 | ||| This is mainly to be used with `Web.Dom.createElement` and `newElement`.
 290 | ||| Some deprecated tags have been left out, some others might
 291 | ||| still be missing.
 292 | public export
 293 | data ElementType : (tag : String) -> (htmlElement : Type) -> Type where
 294 |   A          : ElementType "a" HTMLAnchorElement
 295 |   Address    : ElementType "address" HTMLElement
 296 |   Area       : ElementType "area" HTMLAreaElement
 297 |   Article    : ElementType "article" HTMLElement
 298 |   Audio      : ElementType "audio" HTMLAudioElement
 299 |   Base       : ElementType "base" HTMLBaseElement
 300 |   Blockquote : ElementType "blockquote" HTMLQuoteElement
 301 |   Body       : ElementType "body" HTMLBodyElement
 302 |   Br         : ElementType "br" HTMLBRElement
 303 |   Button     : ElementType "button" HTMLButtonElement
 304 |   Canvas     : ElementType "canvas" HTMLCanvasElement
 305 |   Caption    : ElementType "caption" HTMLTableCaptionElement
 306 |   Col        : ElementType "col" HTMLTableColElement
 307 |   Colgroup   : ElementType "colgroup" HTMLTableColElement
 308 |   Data       : ElementType "data" HTMLDataElement
 309 |   Datalist   : ElementType "datalist" HTMLDataListElement
 310 |   Del        : ElementType "del" HTMLModElement
 311 |   Details    : ElementType "details" HTMLDetailsElement
 312 |   Dialog     : ElementType "dialog" HTMLDialogElement
 313 |   Div        : ElementType "div" HTMLDivElement
 314 |   Dl         : ElementType "dl" HTMLDListElement
 315 |   Embed      : ElementType "embed" HTMLEmbedElement
 316 |   FieldSet   : ElementType "fieldset" HTMLFieldSetElement
 317 |   Footer     : ElementType "footer" HTMLElement
 318 |   Form       : ElementType "form" HTMLFormElement
 319 |   H1         : ElementType "h1" HTMLHeadingElement
 320 |   H2         : ElementType "h2" HTMLHeadingElement
 321 |   H3         : ElementType "h3" HTMLHeadingElement
 322 |   H4         : ElementType "h4" HTMLHeadingElement
 323 |   H5         : ElementType "h5" HTMLHeadingElement
 324 |   H6         : ElementType "h6" HTMLHeadingElement
 325 |   HR         : ElementType "hr" HTMLHRElement
 326 |   Header     : ElementType "header" HTMLElement
 327 |   Html       : ElementType "html" HTMLHtmlElement
 328 |   IFrame     : ElementType "iframe" HTMLIFrameElement
 329 |   Img        : ElementType "img" HTMLImageElement
 330 |   Input      : ElementType "input" HTMLInputElement
 331 |   Ins        : ElementType "ins" HTMLModElement
 332 |   Label      : ElementType "label" HTMLLabelElement
 333 |   Legend     : ElementType "legend" HTMLLegendElement
 334 |   Li         : ElementType "li" HTMLLIElement
 335 |   Link       : ElementType "link" HTMLLinkElement
 336 |   Map        : ElementType "map" HTMLMapElement
 337 |   Menu       : ElementType "menu" HTMLMenuElement
 338 |   Meta       : ElementType "meta" HTMLMetaElement
 339 |   Meter      : ElementType "meter" HTMLMeterElement
 340 |   Object     : ElementType "object" HTMLObjectElement
 341 |   Ol         : ElementType "ol" HTMLOListElement
 342 |   OptGroup   : ElementType "optgroup" HTMLOptGroupElement
 343 |   Option     : ElementType "option" HTMLOptionElement
 344 |   Output     : ElementType "output" HTMLOutputElement
 345 |   P          : ElementType "p" HTMLParagraphElement
 346 |   Param      : ElementType "param" HTMLParamElement
 347 |   Picture    : ElementType "picture" HTMLPictureElement
 348 |   Pre        : ElementType "pre" HTMLPreElement
 349 |   Progress   : ElementType "progress" HTMLProgressElement
 350 |   Q          : ElementType "q" HTMLQuoteElement
 351 |   Script     : ElementType "script" HTMLScriptElement
 352 |   Section    : ElementType "section" HTMLElement
 353 |   Select     : ElementType "select" HTMLSelectElement
 354 |   Slot       : ElementType "slot" HTMLSlotElement
 355 |   Source     : ElementType "source" HTMLSourceElement
 356 |   Span       : ElementType "span" HTMLSpanElement
 357 |   Style      : ElementType "style" HTMLStyleElement
 358 |   Table      : ElementType "table" HTMLTableElement
 359 |   Tbody      : ElementType "tbody" HTMLTableSectionElement
 360 |   Td         : ElementType "td" HTMLTableCellElement
 361 |   Template   : ElementType "template" HTMLTemplateElement
 362 |   TextArea   : ElementType "textarea" HTMLTextAreaElement
 363 |   Tfoot      : ElementType "tfoot" HTMLTableSectionElement
 364 |   Th         : ElementType "th" HTMLTableCellElement
 365 |   Thead      : ElementType "thead" HTMLTableSectionElement
 366 |   Time       : ElementType "time" HTMLTimeElement
 367 |   Title      : ElementType "title" HTMLTitleElement
 368 |   Tr         : ElementType "tr" HTMLTableRowElement
 369 |   Track      : ElementType "track" HTMLTrackElement
 370 |   Ul         : ElementType "ul" HTMLUListElement
 371 |   Video      : ElementType "video" HTMLVideoElement
 372 | 
 373 | ||| Extracts the `tag` String from a known `ElementType`.
 374 | public export %inline
 375 | elementTag : {tag : _} -> (0 _ : ElementType tag t) -> String
 376 | elementTag _ = tag
 377 | 
 378 | ||| Creates a new element using the given `ElementType`'s `tag`
 379 | ||| and casting the result to the corresponding HTML element type.
 380 | ||| See also `newElement`.
 381 | export
 382 | createElement : SafeCast t => {tag : _} -> (0 e : ElementType tag t) -> JSIO t
 383 | createElement e =
 384 |    castingTo "Web.Dom.createElement \{tag}" $ document >>= (`createElement` tag)
 385 | 
 386 | ||| Like `createElement` but applies the given set of
 387 | ||| modifiers. This is especially useful for setting an element's
 388 | ||| attributes.
 389 | export
 390 | newElement :
 391 |      {auto sc : SafeCast t}
 392 |   -> {tag : _}
 393 |   -> (0 e : ElementType tag t)
 394 |   -> (mods : List (t -> JSIO ()))
 395 |   -> JSIO t
 396 | newElement e mods = do
 397 |   res <- createElement e
 398 |   for_ mods $ \m => m res
 399 |   pure res
 400 | 
 401 | --------------------------------------------------------------------------------
 402 | --          Finding Elements
 403 | --------------------------------------------------------------------------------
 404 | 
 405 | export
 406 | ArrayLike HTMLCollection Element where
 407 | 
 408 | export
 409 | getElementById : String -> JSIO (Maybe Element)
 410 | getElementById s = document >>= (`getElementById` s)
 411 | 
 412 | export
 413 | castElementById_ : SafeCast a => String -> JSIO (Maybe a)
 414 | castElementById_ = map (>>= safeCast) . getElementById
 415 | 
 416 | export %inline
 417 | castElementById : (0 a : Type) -> SafeCast a => String -> JSIO (Maybe a)
 418 | castElementById _ = castElementById_
 419 | 
 420 | export %inline
 421 | htmlElementById :
 422 |      {auto sc : SafeCast t}
 423 |   -> (0 e : ElementType tag t)
 424 |   -> String
 425 |   -> JSIO (Maybe t)
 426 | htmlElementById e s = castElementById_ s
 427 | 
 428 | export
 429 | getElementsByClass : String -> JSIO HTMLCollection
 430 | getElementsByClass s = document >>= (`getElementsByClassName` s)
 431 | 
 432 | export
 433 | firstElementByClass : String -> JSIO (Maybe Element)
 434 | firstElementByClass s = do
 435 |   col <- getElementsByClass s
 436 |   readIO col 0
 437 | 
 438 | export
 439 | castFirstElementByClass_ : SafeCast a => String -> JSIO (Maybe a)
 440 | castFirstElementByClass_ = map (>>= safeCast) . firstElementByClass
 441 | 
 442 | export %inline
 443 | castFirstElementByClass :
 444 |      (0 a : Type)
 445 |   -> {auto sc : SafeCast a}
 446 |   -> String
 447 |   -> JSIO (Maybe a)
 448 | castFirstElementByClass _ = castFirstElementByClass_
 449 | 
 450 | export %inline
 451 | firstHtmlElementByClass :
 452 |      (0 e : ElementType tag a)
 453 |   -> {auto sc : SafeCast a}
 454 |   -> String
 455 |   -> JSIO (Maybe a)
 456 | firstHtmlElementByClass e s = castFirstElementByClass_ s
 457 | 
 458 | ||| Tries to retrieve an element of the given type by looking
 459 | ||| up its class in the DOM. Unlike `firstElementByClass`, this will throw
 460 | ||| an exception in the `JSIO` monad if the element is not found
 461 | ||| or can't be safely cast to the desired type.
 462 | export
 463 | getElementByClass : SafeCast t => (class : String) -> JSIO t
 464 | getElementByClass class = liftJSIO $ do
 465 |   Nothing <- castFirstElementByClass t class | Just t => pure t
 466 |   throwError $ Caught "Web.Dom.getElementByClass: Could not find an element with class \{class}"
 467 | 
 468 | --------------------------------------------------------------------------------
 469 | --          Interfaces
 470 | --------------------------------------------------------------------------------
 471 | 
 472 | export
 473 | ArrayLike NodeList Node where
 474 | 
 475 | export
 476 | ArrayLike DOMTokenList String where
 477 | 
 478 | export
 479 | Callback EventListener (Event -> JSIO ()) where
 480 |   callback f = toEventListener (runJS . f)
 481 | 
 482 | export
 483 | Callback MutationCallback
 484 |   (Array MutationRecord -> MutationObserver -> JSIO ()) where
 485 |   callback f = toMutationCallback $ \a,m => runJS (f a m)
 486 | 
 487 | ||| In case of an error, the error is logged to the console and
 488 | ||| the node is rejected
 489 | export
 490 | Callback NodeFilter (Node -> JSIO Bits16) where
 491 |   callback f = toNodeFilter (runJSWithDefault FILTER_REJECT . f)
 492 | 
 493 | export
 494 | Callback XPathNSResolver (Maybe String -> JSIO (Maybe String) ) where
 495 |   callback f =
 496 |     toXPathNSResolver $
 497 |         map maybeToNullable
 498 |       . runJSWithDefault Nothing
 499 |       . f
 500 |       . nullableToMaybe
 501 |