
   0 | module Web.Async.Util
   1 | 
   2 | import Data.Array
   3 | import Data.Buffer
   4 | import Data.Vect
   5 | import Web.Async.Event
   6 | import Web.Internal.Types
   7 | import public FS
   8 | import public FS.Concurrent.Signal
   9 | import public IO.Async.JS
  10 | import public JS
  11 | import public Text.HTML
  12 | 
  13 | %default total
  14 | 
  15 | --------------------------------------------------------------------------------
  16 | --          FFI
  17 | --------------------------------------------------------------------------------
  18 | 
  19 | %foreign "javascript:lambda:x=>x.length"
  20 | prim__buflen : Buffer -> Bits32
  21 | 
  22 | %foreign "browser:lambda:(w)=>window"
  23 | prim__window : PrimIO Window
  24 | 
  25 | %foreign "browser:lambda:(w)=>document"
  26 | prim__document : PrimIO Document
  27 | 
  28 | %foreign "browser:lambda:(w)=>document.body"
  29 | prim__body : PrimIO (Nullable HTMLElement)
  30 | 
  31 | %foreign "browser:lambda:(x,w)=>document.getElementById(x)"
  32 | prim__getElementById : String -> PrimIO (Nullable Element)
  33 | 
  34 | %foreign "browser:lambda:(x,s,w)=>x.setCustomValidity(s)"
  35 | prim__setCustomValidity : Element -> String -> PrimIO ()
  36 | 
  37 | %foreign "browser:lambda:(x,s,w)=> {x.value = s;}"
  38 | prim__setValue : Element -> String -> PrimIO ()
  39 | 
  40 | %foreign "browser:lambda:(x,w)=> x.click()"
  41 | prim__click : HTMLElement -> PrimIO ()
  42 | 
  43 | %foreign "browser:lambda:(x,n,w)=>x.replaceChildren(n)"
  44 | prim__replaceChildren : ParentNode -> Node -> PrimIO ()
  45 | 
  46 | export
  47 | %foreign "browser:lambda:(x,n,w)=>x.append(n)"
  48 | prim__append : ParentNode -> Node -> PrimIO ()
  49 | 
  50 | export
  51 | %foreign "browser:lambda:(x,n,w)=>x.append(n)"
  52 | prim__appendTxt : ParentNode -> String -> PrimIO ()
  53 | 
  54 | %foreign "browser:lambda:(x,n,w)=>x.prepend(n)"
  55 | prim__prepend : ParentNode -> Node -> PrimIO ()
  56 | 
  57 | %foreign "browser:lambda:(x,n,w)=>x.after(n)"
  58 | prim__after : ChildNode -> Node -> PrimIO ()
  59 | 
  60 | %foreign "browser:lambda:(x,n,w)=>x.before(n)"
  61 | prim__before : ChildNode -> Node -> PrimIO ()
  62 | 
  63 | %foreign "browser:lambda:(x,n,w)=>x.replaceWith(n)"
  64 | prim__replace : ChildNode -> Node -> PrimIO ()
  65 | 
  66 | export
  67 | %foreign "browser:lambda:(x,w)=>x.remove()"
  68 | prim__remove : ChildNode -> PrimIO ()
  69 | 
  70 | export
  71 | %foreign "browser:lambda:(s,w)=>document.createElement(s)"
  72 | prim__createElement : String -> PrimIO Element
  73 | 
  74 | export
  75 | %foreign "browser:lambda:(x,a,b,w)=>x.setAttribute(a,b)"
  76 | prim__setAttribute : Element -> String -> String -> PrimIO ()
  77 | 
  78 | export
  79 | %foreign "browser:lambda:(x,a,w)=>x.removeAttribute(a)"
  80 | prim__removeAttribute : Element -> String -> PrimIO ()
  81 | 
  82 | export
  83 | %foreign "browser:lambda:(x,w)=>x.innerHTML"
  84 | prim__innerHTML : InnerHTML -> PrimIO String
  85 | 
  86 | export
  87 | %foreign "browser:lambda:(x,v,w)=>{x.innerHTML = v}"
  88 | prim__setInnerHTML : InnerHTML -> String -> PrimIO ()
  89 | 
  90 | export
  91 | %foreign "browser:lambda:(x,w)=>x.content"
  92 | prim__content : HTMLTemplateElement -> PrimIO DocumentFragment
  93 | 
  94 | export
  95 | %foreign "browser:lambda:w=>document.createDocumentFragment()"
  96 | prim__createDocumentFragment : PrimIO DocumentFragment
  97 | 
  98 | export
  99 | %foreign "browser:lambda:(x,v,w)=>{x.checked = v}"
 100 | prim__setChecked : HTMLInputElement -> Boolean -> PrimIO ()
 101 | 
 102 | export
 103 | %foreign "browser:lambda:(x,v,w)=>x.checked?1:0"
 104 | prim__checked : HTMLInputElement -> PrimIO Bool
 105 | 
 106 | %foreign "browser:lambda:(x,w)=>x.blur()"
 107 | prim__blur : HTMLOrSVGElement -> PrimIO ()
 108 | 
 109 | %foreign "browser:lambda:(x,w)=>x.focus()"
 110 | prim__focus : HTMLOrSVGElement -> PrimIO ()
 111 | 
 112 | -- TODO: This should go to the js library
 113 | %foreign "javascript:lambda:(w) => BigInt(new Date().getTime())"
 114 | prim__time : PrimIO Integer
 115 | 
 116 | %foreign "browser:lambda:(s,w) => navigator.clipboard.writeText(s)"
 117 | prim__writeToClipboard : String -> PrimIO ()
 118 | 
 119 | %foreign "browser:lambda:(i,w) => navigator.clipboard.write([i])"
 120 | prim__itemToClipboard : ClipboardItem -> PrimIO (Promise ())
 121 | 
 122 | %foreign "browser:lambda:(m,s,w) => new ClipboardItem({[m]: s})"
 123 | prim__clipboardItem : (mimeType, content : String) -> PrimIO ClipboardItem
 124 | 
 125 | %foreign "browser:lambda:(f,w) => navigator.clipboard.readText().then(s => f(s)(w))"
 126 | prim__readFromClipboard : (String -> PrimIO ()) -> PrimIO ()
 127 | 
 128 | %foreign "browser:lambda:(e,w) => e.getBoundingClientRect()"
 129 | prim__getBoundingClientRect : Element -> PrimIO DOMRect
 130 | 
 131 | %foreign "browser:lambda:(e,w) => e.show()"
 132 | prim__dialogShow : HTMLDialogElement -> PrimIO ()
 133 | 
 134 | %foreign "browser:lambda:(e,w) => e.close()"
 135 | prim__dialogClose : HTMLDialogElement -> PrimIO ()
 136 | 
 137 | %foreign "browser:lambda:(e,w) => e.showModal()"
 138 | prim__showModal : HTMLDialogElement -> PrimIO ()
 139 | 
 140 | %foreign "browser:lambda:(p,s,w) => new Blob(p, {type:s})"
 141 | prim__blob : AnyPtr -> String -> PrimIO Blob
 142 | 
 143 | %foreign "browser:lambda:(b,w) => b.bytes()"
 144 | prim__blobBytes : Blob -> PrimIO (Promise Buffer)
 145 | 
 146 | %foreign "browser:lambda:(b,w) => URL.createObjectURL(b)"
 147 | prim__blobURL : Blob -> PrimIO String
 148 | 
 149 | %foreign "browser:lambda:(u,w) => URL.revokeObjectURL(u)"
 150 | prim__revokeObjectURL : String -> PrimIO ()
 151 | 
 152 | --------------------------------------------------------------------------------
 153 | --          Core Utilities
 154 | --------------------------------------------------------------------------------
 155 | 
 156 | ||| Return the current window.
 157 | export %inline
 158 | window : HasIO io => io Window
 159 | window = primIO prim__window
 160 | 
 161 | ||| Return the current document.
 162 | export %inline
 163 | document : HasIO io => io Document
 164 | document = primIO prim__document
 165 | 
 166 | ||| Return the body element of the current document.
 167 | |||
 168 | ||| Return `Nothing` in case the current document has no body defined.
 169 | export
 170 | getBody : HasIO io => io (Maybe HTMLElement)
 171 | getBody = nullableToMaybe <$> primIO prim__body
 172 | 
 173 | ||| Simulates a mouse click on an element.
 174 | export %inline
 175 | click : HasIO io => HTMLElement -> io ()
 176 | click x = primIO (prim__click x)
 177 | 
 178 | ||| Replace all children of the given node with a new node.
 179 | export %inline
 180 | replaceChildren : HasIO io => ParentNode -> Node -> io ()
 181 | replaceChildren el n = primIO $ prim__replaceChildren el n
 182 | 
 183 | ||| Append the given node to a DOM element's children
 184 | export %inline
 185 | append : HasIO io => ParentNode -> Node -> io ()
 186 | append el n = primIO $ prim__append el n
 187 | 
 188 | ||| Prepend the given node to a DOM element's children
 189 | export %inline
 190 | prepend : HasIO io => ParentNode -> Node -> io ()
 191 | prepend el n = primIO $ prim__prepend el n
 192 | 
 193 | ||| Insert the given node after a DOM element
 194 | export %inline
 195 | after : HasIO io => ChildNode -> Node -> io ()
 196 | after el n = primIO $ prim__after el n
 197 | 
 198 | ||| Insert the given node before a DOM element
 199 | export %inline
 200 | before : HasIO io => ChildNode -> Node -> io ()
 201 | before el n = primIO $ prim__before el n
 202 | 
 203 | ||| Replace a DOM element with the given node.
 204 | export %inline
 205 | replace : HasIO io => ChildNode -> Node -> io ()
 206 | replace el n = primIO $ prim__replace el n
 207 | 
 208 | ||| Replace a DOM element with the given document fragment.
 209 | export %inline
 210 | remove : HasIO io => ChildNode -> io ()
 211 | remove el = primIO $ prim__remove el
 212 | 
 213 | ||| Creates a DOM element of the given type.
 214 | export %inline
 215 | createElement : HasIO io => String -> io Element
 216 | createElement s = primIO $ prim__createElement s
 217 | 
 218 | ||| Sets an attribute of a DOM element.
 219 | export %inline
 220 | setAttribute : HasIO io => Element -> (name, value : String) -> io ()
 221 | setAttribute el n v = primIO $ prim__setAttribute el n v
 222 | 
 223 | ||| Unsets an attribute of a DOM element.
 224 | export %inline
 225 | removeAttribute : HasIO io => Element -> (name : String) -> io ()
 226 | removeAttribute el n = primIO $ prim__removeAttribute el n
 227 | 
 228 | ||| Returns the inner HTML structure of a node as a String
 229 | export %inline
 230 | innerHTML : HasIO io => InnerHTML -> io String
 231 | innerHTML n = primIO $ prim__innerHTML n
 232 | 
 233 | ||| Sets the inner HTML structure of a node.
 234 | export %inline
 235 | setInnerHTML : HasIO io => InnerHTML -> String -> io ()
 236 | setInnerHTML n s = primIO $ prim__setInnerHTML n s
 237 | 
 238 | ||| Focus the given HTML element
 239 | export %inline
 240 | focus : HasIO io => HTMLElement -> io ()
 241 | focus el = primIO (prim__focus $ up el)
 242 | 
 243 | ||| Blur (lose focus of) the given HTML element
 244 | export %inline
 245 | blur : HasIO io => HTMLElement -> io ()
 246 | blur el = primIO (prim__blur $ up el)
 247 | 
 248 | ||| Get the current time in milliseconds since 1970/01/01.
 249 | export
 250 | currentTime : HasIO io => io Integer
 251 | currentTime = primIO prim__time
 252 | 
 253 | ||| Determine the time taken to run an `IO` action.
 254 | export
 255 | timed : HasIO io => io t -> io (t,Integer)
 256 | timed act = do
 257 |   t1 <- currentTime
 258 |   v  <- act
 259 |   t2 <- currentTime
 260 |   pure (v, t2 - t1)
 261 | 
 262 | export %inline
 263 | timed' : HasIO io => io () -> io Integer
 264 | timed' = map snd . timed
 265 | 
 266 | ||| Writes as string to the clipboard.
 267 | export %inline
 268 | toClipboard : HasIO io => String -> io ()
 269 | toClipboard s = primIO (prim__writeToClipboard s)
 270 | 
 271 | ||| Writes a `ClipboardItem` to the clipboard.
 272 | export
 273 | itemToClipboard : Elem JSErr es => ClipboardItem -> Async JS es ()
 274 | itemToClipboard ci = do
 275 |   p <- primIO (prim__itemToClipboard ci)
 276 |   promise p
 277 | 
 278 | ||| Wraps some text data plus its mimetype in a `ClipboardItem`
 279 | export %inline
 280 | clipboardItem : HasIO io => (mimetype, content : String) -> io ClipboardItem
 281 | clipboardItem m s = primIO (prim__clipboardItem m s)
 282 | 
 283 | ||| Writes some text data plus its mimetype to the clipboard.
 284 | export
 285 | dataToClipboard : Elem JSErr es => (mimetype, content : String) -> Async JS es ()
 286 | dataToClipboard m c = clipboardItem m c >>= itemToClipboard
 287 | 
 288 | export
 289 | readFromClipboard1 : HasIO io => (String -> IO1 ()) -> io ()
 290 | readFromClipboard1 cb = primIO $ prim__readFromClipboard (\s => primRun (cb s))
 291 | 
 292 | export
 293 | readFromClipboard : Async e es String
 294 | readFromClipboard =
 295 |   primAsync_ $ \cb =>
 296 |     ffi $ prim__readFromClipboard (\s => primRun (cb $ Right s))
 297 | 
 298 | ||| Show the given dialog element
 299 | export %inline
 300 | dialogShow : HasIO io => HTMLDialogElement -> io ()
 301 | dialogShow el = primIO (prim__dialogShow el)
 302 | 
 303 | ||| Close the given dialog element
 304 | export %inline
 305 | dialogClose : HasIO io => HTMLDialogElement -> io ()
 306 | dialogClose el = primIO (prim__dialogClose el)
 307 | 
 308 | ||| Show the given dialog element in "modal" mode
 309 | export %inline
 310 | showModal : HasIO io => HTMLDialogElement -> io ()
 311 | showModal el = primIO (prim__showModal el)
 312 | 
 313 | --------------------------------------------------------------------------------
 314 | --          Blobs
 315 | --------------------------------------------------------------------------------
 316 | 
 317 | public export
 318 | interface ToBlob a where
 319 |   toBlob : a -> AnyPtr
 320 | 
 321 | export %inline
 322 | ToBlob (IArray k String) where
 323 |   toBlob = unsafeToPtr
 324 | 
 325 | export %inline
 326 | ToBlob (Indexed.Array String) where
 327 |   toBlob (A _ arr) = toBlob arr
 328 | 
 329 | export %inline
 330 | ToBlob (List String) where
 331 |   toBlob s = toBlob (arrayL s)
 332 | 
 333 | export %inline
 334 | ToBlob String where
 335 |   toBlob s = toBlob $ array [s]
 336 | 
 337 | export
 338 | blob : {0 a : _} -> HasIO io =>  ToBlob a => a -> (mimetype : String) -> io Blob
 339 | blob v mimetype = primIO (prim__blob (toBlob v) mimetype)
 340 | 
 341 | ||| A URL (as a wrapped string) pointing to an object in memory.
 342 | |||
 343 | ||| This should be treated as a resource and properly released via `cleanup`.
 344 | export
 345 | record ObjectURL where
 346 |   constructor OU
 347 |   url : String
 348 | 
 349 | export %inline
 350 | Resource (Async JS) ObjectURL where
 351 |   cleanup (OU u) = primIO (prim__revokeObjectURL u)
 352 | 
 353 | export %inline
 354 | Cast ObjectURL String where cast = url
 355 | 
 356 | ||| Provides a URL pointing to the given `Blob` object.
 357 | |||
 358 | ||| Use `cast` to convert the `ObjectURL` to a `String` and make sure to
 359 | ||| release it
 360 | export %inline
 361 | blobURL : HasIO io => Blob -> io ObjectURL
 362 | blobURL b = OU <$> primIO (prim__blobURL b)
 363 | 
 364 | ||| Extracts the bytes from a `Blob`.
 365 | export
 366 | blobBytes : Has JSErr es => Blob -> Async JS es AnyBuffer
 367 | blobBytes b = Prelude.do
 368 |   pbuf <- primIO (prim__blobBytes b)
 369 |   buf  <- promise pbuf
 370 |   pure $ AB (cast $ prim__buflen buf) (unsafeMakeBuffer buf)
 371 | 
 372 | --------------------------------------------------------------------------------
 373 | --          Type Computations
 374 | --------------------------------------------------------------------------------
 375 | 
 376 | ||| DOM type associacte with an ElemRef
 377 | public export
 378 | 0 ElemType : Ref t -> Type
 379 | ElemType (Id _)   = Element
 380 | ElemType (Elem _) = Element
 381 | ElemType Body     = HTMLElement
 382 | ElemType Document = Document
 383 | ElemType Window   = Window
 384 | 
 385 | public export
 386 | 0 JS : List Type -> Type -> Type
 387 | JS = Async JS
 388 | 
 389 | nodeList : DocumentFragment -> List (HSum [Node,String])
 390 | nodeList df = [inject $ df :> Node]
 391 | 
 392 | --------------------------------------------------------------------------------
 393 | --          Accessing and Updating Nodes
 394 | --------------------------------------------------------------------------------
 395 | 
 396 | parameters {auto has : Has JSErr es}
 397 | 
 398 |   export %inline
 399 |   js : JSIO t -> JS es t
 400 |   js = injectIO . runEitherT
 401 | 
 402 |   export
 403 |   jsCast : SafeCast t => String -> s -> JS es t
 404 |   jsCast msg = js . tryCast msg
 405 | 
 406 |   export
 407 |   unmaybe : Lazy String -> Maybe t -> JS es t
 408 |   unmaybe msg = maybe (throw $ Caught msg) pure
 409 | 
 410 |   export
 411 |   body : JS es HTMLElement
 412 |   body = getBody >>= unmaybe "document.body returned `Nothing`"
 413 | 
 414 |   ||| Tries to retrieve an element of the given type by looking
 415 |   ||| up its ID in the DOM.
 416 |   |||
 417 |   ||| This will throw a `JSErr` in case the element cannot be found
 418 |   ||| or cast to the desired result type.
 419 |   export
 420 |   getElementById : SafeCast t => Maybe String -> (id : String) -> JS es t
 421 |   getElementById mtag id = do
 422 |     e <- primIO (prim__getElementById id)
 423 |     unmaybe msg $ nullableToMaybe e >>= castTo t
 424 |     where
 425 |       %inline tag, msg : String
 426 |       tag = fromMaybe "element" mtag
 427 |       msg = "getElementById: Could not find \{tag} with id \{id}"
 428 | 
 429 |   ||| Tries to retrieve a HTMLElement by looking
 430 |   |||
 431 |   ||| This will throw a `JSErr` in case the element cannot be found
 432 |   ||| or cast to the desired result type.
 433 |   export %inline
 434 |   getHTMLElementById : (tag,id : String) -> JS es HTMLElement
 435 |   getHTMLElementById = getElementById . Just
 436 | 
 437 |   ||| Tries to retrieve an element of the given type by looking
 438 |   ||| up its ID in the DOM.
 439 |   |||
 440 |   ||| This will throw a `JSErr` in case the element cannot be found
 441 |   ||| or cast to the desired result type.
 442 |   export
 443 |   getElementByRef : (r : Ref t) -> JS es (ElemType r)
 444 |   getElementByRef (Id {tag} id) = getElementById (Just tag) id
 445 |   getElementByRef (Elem id)     = getElementById Nothing id
 446 |   getElementByRef Body          = body
 447 |   getElementByRef Document      = document
 448 |   getElementByRef Window        = window
 449 | 
 450 |   err : String
 451 |   err = "Web.Async.getElementByRef"
 452 | 
 453 |   ||| Tries to retrieve an element of the given type by looking
 454 |   ||| up its ID in the DOM.
 455 |   |||
 456 |   ||| This will throw a `JSErr` in case the element cannot be found
 457 |   ||| or cast to the desired result type.
 458 |   export
 459 |   castElementByRef : {0 x : k} -> SafeCast t => Ref x -> JS es t
 460 |   castElementByRef ref = getElementByRef ref >>= jsCast err
 461 | 
 462 |   ||| Sets a custom validity message at the given reference.
 463 |   |||
 464 |   ||| Pass the empty string to mark the element as valid.
 465 |   |||
 466 |   ||| This will throw a `JSErr` in case the element cannot be found
 467 |   ||| or cast to the desired result type.
 468 |   export %inline
 469 |   validityMessage : Ref t -> (0 p : ValidityTag t) => String -> JS es ()
 470 |   validityMessage r s =
 471 |     castElementByRef r >>= \e => primIO (prim__setCustomValidity e s)
 472 | 
 473 |   ||| Sets or unsets a custom validity message at the given node.
 474 |   export
 475 |   validate : Ref t -> (0 p : ValidityTag t) => Either String b -> JS es ()
 476 |   validate r (Left s)  = validityMessage r s
 477 |   validate r (Right s) = validityMessage r ""
 478 | 
 479 |   ||| Sets the value of the element identified by the given ID.
 480 |   |||
 481 |   ||| This will throw a `JSErr` in case the element cannot be found
 482 |   ||| or cast to the desired result type.
 483 |   export %inline
 484 |   setValue : Ref t -> (0 p : ValueTag t) => String -> JS es ()
 485 |   setValue r s = castElementByRef r >>= \e => primIO (prim__setValue e s)
 486 | 
 487 | --------------------------------------------------------------------------------
 488 | --          DOM Streams
 489 | --------------------------------------------------------------------------------
 490 | 
 491 | public export
 492 | 0 Act : Type -> Type
 493 | Act = Async JS [JSErr]
 494 | 
 495 | public export
 496 | 0 JSPull : Type -> Type -> Type
 497 | JSPull o r = Pull (Async JS) o [JSErr] r
 498 | 
 499 | public export
 500 | 0 JSStream : Type -> Type
 501 | JSStream o = Pull (Async JS) o [JSErr] ()
 502 | 
 503 | export covering
 504 | pullErr : AsyncStream f es Void -> Async f es ()
 505 | pullErr s =
 506 |   weakenErrors (pull s) >>= \case
 507 |     Error err => fail err
 508 |     _         => pure ()
 509 | 
 510 | export covering %inline
 511 | runJS : JS [JSErr] () -> IO ()
 512 | runJS = app . handle [putStrLn . dispErr]
 513 | 
 514 | export covering %inline
 515 | runProg : JSStream Void -> IO ()
 516 | runProg = runJS . pullErr
 517 | 
 518 | export
 519 | mvcActEvs : JSStream e -> s -> (e -> s -> Act s) -> JSStream Void
 520 | mvcActEvs evs ini act = evs |> P.evalScans1 ini (flip act) |> drain
 521 | 
 522 | parameters (ev  : e)
 523 |            (ini : s)
 524 | 
 525 |   export
 526 |   mvcAct : (Sink e => e -> s -> Act s) -> JSStream Void
 527 |   mvcAct act = do
 528 |     E evs <- exec $ eventFrom ev
 529 |     mvcActEvs evs ini act
 530 | 
 531 |   export
 532 |   mvc : (e -> s -> s) -> (Sink e => e -> s -> Act ()) -> JSStream Void
 533 |   mvc upd disp =
 534 |     mvcAct (\v,x => let y := upd v x in disp v y $> y)
 535 | 
 536 | --------------------------------------------------------------------------------
 537 | --          Geometry
 538 | --------------------------------------------------------------------------------
 539 | 
 540 | export
 541 | getClientRect : LIO f => Element -> f Rect
 542 | getClientRect el = Prelude.do
 543 |   r <- lift1 $ ffi (prim__getBoundingClientRect el)
 544 |   lift1 (toRect r)
 545 |