0 | module Web.Async.Util

  2 | import Data.Array

  3 | import Data.ByteString

  4 | import Data.Buffer

  5 | import Data.Vect

  6 | import HTTP.API.Client.FFI

  7 | import Web.Async.Event

  8 | import Web.Internal.Types

  9 | import public FS

 10 | import public FS.Concurrent.Signal

 11 | import public IO.Async.JS

 12 | import public JS

 13 | import public Text.HTML

 15 | %default total

 21 | %foreign "javascript:lambda:x=>x.length"

 22 | prim__buflen : Buffer -> Bits32

 24 | %foreign "browser:lambda:(w)=>window"

 25 | prim__window : PrimIO Window

 27 | %foreign "browser:lambda:(w)=>document"

 28 | prim__document : PrimIO Document

 30 | %foreign "browser:lambda:(w)=>document.body"

 31 | prim__body : PrimIO (Nullable HTMLElement)

 33 | %foreign "browser:lambda:(x,w)=>document.getElementById(x)"

 34 | prim__getElementById : String -> PrimIO (Nullable Element)

 36 | %foreign "browser:lambda:(x,s,w)=>x.setCustomValidity(s)"

 37 | prim__setCustomValidity : Element -> String -> PrimIO ()

 39 | %foreign "browser:lambda:(x,s,w)=> {x.value = s;}"

 40 | prim__setValue : Element -> String -> PrimIO ()

 42 | %foreign "browser:lambda:(x,w)=> x.click()"

 43 | prim__click : HTMLElement -> PrimIO ()

 45 | %foreign "browser:lambda:(x,n,w)=>x.replaceChildren(n)"

 46 | prim__replaceChildren : ParentNode -> Node -> PrimIO ()

 49 | %foreign "browser:lambda:(x,n,w)=>x.append(n)"

 50 | prim__append : ParentNode -> Node -> PrimIO ()

 53 | %foreign "browser:lambda:(x,n,w)=>x.append(n)"

 54 | prim__appendTxt : ParentNode -> String -> PrimIO ()

 56 | %foreign "browser:lambda:(x,n,w)=>x.prepend(n)"

 57 | prim__prepend : ParentNode -> Node -> PrimIO ()

 59 | %foreign "browser:lambda:(x,n,w)=>x.after(n)"

 60 | prim__after : ChildNode -> Node -> PrimIO ()

 62 | %foreign "browser:lambda:(x,n,w)=>x.before(n)"

 63 | prim__before : ChildNode -> Node -> PrimIO ()

 65 | %foreign "browser:lambda:(x,n,w)=>x.replaceWith(n)"

 66 | prim__replace : ChildNode -> Node -> PrimIO ()

 69 | %foreign "browser:lambda:(x,w)=>x.remove()"

 70 | prim__remove : ChildNode -> PrimIO ()

 73 | %foreign "browser:lambda:(x,w)=>x.nextSibling"

 74 | prim__nextSibling : ChildNode -> PrimIO (Nullable ChildNode)

 76 | %foreign "browser:lambda:(x,y,w)=>x.isEqualNode(y)?1:0"

 77 | prim__doRemove : ChildNode -> ChildNode -> PrimIO Bits8

 80 | %foreign "browser:lambda:(s,w)=>document.createElement(s)"

 81 | prim__createElement : String -> PrimIO Element

 84 | %foreign "browser:lambda:(x,a,b,w)=>x.setAttribute(a,b)"

 85 | prim__setAttribute : Element -> String -> String -> PrimIO ()

 88 | %foreign "browser:lambda:(x,a,w)=>x.removeAttribute(a)"

 89 | prim__removeAttribute : Element -> String -> PrimIO ()

 92 | %foreign "browser:lambda:(x,w)=>x.innerHTML"

 93 | prim__innerHTML : InnerHTML -> PrimIO String

 96 | %foreign "browser:lambda:(x,v,w)=>{x.innerHTML = v}"

 97 | prim__setInnerHTML : InnerHTML -> String -> PrimIO ()

100 | %foreign "browser:lambda:(x,w)=>x.content"

101 | prim__content : HTMLTemplateElement -> PrimIO DocumentFragment

104 | %foreign "browser:lambda:w=>document.createDocumentFragment()"

105 | prim__createDocumentFragment : PrimIO DocumentFragment

108 | %foreign "browser:lambda:(x,v,w)=>{x.checked = v}"

109 | prim__setChecked : HTMLInputElement -> Boolean -> PrimIO ()

112 | %foreign "browser:lambda:(x,v,w)=>x.checked?1:0"

113 | prim__checked : HTMLInputElement -> PrimIO Bool

115 | %foreign "browser:lambda:(x,w)=>x.blur()"

116 | prim__blur : HTMLOrSVGElement -> PrimIO ()

118 | %foreign "browser:lambda:(x,w)=>x.focus()"

119 | prim__focus : HTMLOrSVGElement -> PrimIO ()

122 | %foreign "javascript:lambda:(w) => BigInt(new Date().getTime())"

123 | prim__time : PrimIO Integer

125 | %foreign "browser:lambda:(s,w) => navigator.clipboard.writeText(s)"

126 | prim__writeToClipboard : String -> PrimIO ()

128 | %foreign "browser:lambda:(i,w) => navigator.clipboard.write([i])"

129 | prim__itemToClipboard : ClipboardItem -> PrimIO (Promise ())

131 | %foreign "browser:lambda:(m,s,w) => new ClipboardItem({[m]: s})"

132 | prim__clipboardItem : (mimeType, content : String) -> PrimIO ClipboardItem

134 | %foreign "browser:lambda:(f,w) => navigator.clipboard.readText().then(s => f(s)(w))"

135 | prim__readFromClipboard : (String -> PrimIO ()) -> PrimIO ()

137 | %foreign "browser:lambda:(e,w) => e.getBoundingClientRect()"

138 | prim__getBoundingClientRect : Element -> PrimIO DOMRect

140 | %foreign "browser:lambda:(e,w) => e.show()"

141 | prim__dialogShow : HTMLDialogElement -> PrimIO ()

143 | %foreign "browser:lambda:(e,w) => e.close()"

144 | prim__dialogClose : HTMLDialogElement -> PrimIO ()

146 | %foreign "browser:lambda:(e,w) => e.showModal()"

147 | prim__showModal : HTMLDialogElement -> PrimIO ()

149 | %foreign "browser:lambda:(p,s,w) => new Blob(p, {type:s})"

150 | prim__blob : AnyPtr -> String -> PrimIO Blob

152 | %foreign "browser:lambda:(b,w) => b.bytes()"

153 | prim__blobBytes : Blob -> PrimIO (Promise Buffer)

155 | %foreign "browser:lambda:(b,w) => URL.createObjectURL(b)"

156 | prim__blobURL : Blob -> PrimIO String

158 | %foreign "browser:lambda:(u,w) => URL.revokeObjectURL(u)"

159 | prim__revokeObjectURL : String -> PrimIO ()

162 | data Reader : Type where [external]

164 | %foreign "browser:lambda:(b,w) => b.stream().getReader()"

165 | prim__blobReader : Blob -> PrimIO Reader

167 | %foreign "browser:lambda:(r,w) => r.cancel()"

168 | prim__cancelRead : Reader -> PrimIO ()

170 | %foreign "browser:lambda:(r,w) => r.read()"

171 | prim__readChunk : Reader -> PrimIO (Promise AnyPtr)

173 | %foreign "browser:lambda:(r) => r.done?1:0"

174 | prim__isDone : AnyPtr -> Bits8

176 | %foreign "browser:lambda:(r) => new UInt8Array(r.value)"

177 | prim__buf : AnyPtr -> Buffer

184 | export %inline

185 | window : HasIO io => io Window

186 | window = primIO prim__window

189 | export %inline

190 | document : HasIO io => io Document

191 | document = primIO prim__document

197 | getBody : HasIO io => io (Maybe HTMLElement)

198 | getBody = nullableToMaybe <$> primIO prim__body

201 | export %inline

202 | click : HasIO io => HTMLElement -> io ()

203 | click x = primIO (prim__click x)

206 | export %inline

207 | replaceChildren : HasIO io => ParentNode -> Node -> io ()

208 | replaceChildren el n = primIO $ prim__replaceChildren el n

211 | export %inline

212 | append : HasIO io => ParentNode -> Node -> io ()

213 | append el n = primIO $ prim__append el n

216 | export %inline

217 | prepend : HasIO io => ParentNode -> Node -> io ()

218 | prepend el n = primIO $ prim__prepend el n

221 | export %inline

222 | after : HasIO io => ChildNode -> Node -> io ()

223 | after el n = primIO $ prim__after el n

226 | export %inline

227 | before : HasIO io => ChildNode -> Node -> io ()

228 | before el n = primIO $ prim__before el n

231 | export %inline

232 | replace : HasIO io => ChildNode -> Node -> io ()

233 | replace el n = primIO $ prim__replace el n

236 | export %inline

237 | remove : HasIO io => ChildNode -> io ()

238 | remove el = primIO $ prim__remove el

243 | removeTill : HasIO io => ChildNode -> ChildNode -> io ()

244 | removeTill x y = primIO go

245 |   where

246 |     go : PrimIO ()

247 |     go w =

248 |      let MkIORes m w := prim__nextSibling x w

249 |          MkIORes _ w := toPrim (putStrLn "removing node") w

250 |          Just n      := nullableToMaybe m    | Nothing => MkIORes () w

251 |          MkIORes 0 w := prim__doRemove y n w | MkIORes _ w => MkIORes () w

252 |          MkIORes _ w := prim__remove n w

253 |          MkIORes _ w := toPrim (putStrLn "removed node") w

254 |       in assert_total $ go w

257 | export %inline

258 | createElement : HasIO io => String -> io Element

259 | createElement s = primIO $ prim__createElement s

262 | export %inline

263 | setAttribute : HasIO io => Element -> (name, value : String) -> io ()

264 | setAttribute el n v = primIO $ prim__setAttribute el n v

267 | export %inline

268 | removeAttribute : HasIO io => Element -> (name : String) -> io ()

269 | removeAttribute el n = primIO $ prim__removeAttribute el n

272 | export %inline

273 | innerHTML : HasIO io => InnerHTML -> io String

274 | innerHTML n = primIO $ prim__innerHTML n

277 | export %inline

278 | setInnerHTML : HasIO io => InnerHTML -> String -> io ()

279 | setInnerHTML n s = primIO $ prim__setInnerHTML n s

282 | export %inline

283 | focus : HasIO io => HTMLElement -> io ()

284 | focus el = primIO (prim__focus $ up el)

287 | export %inline

288 | blur : HasIO io => HTMLElement -> io ()

289 | blur el = primIO (prim__blur $ up el)

293 | currentTime : HasIO io => io Integer

294 | currentTime = primIO prim__time

298 | timed : HasIO io => io t -> io (t,Integer)

299 | timed act = do

300 |   t1 <- currentTime

301 |   v  <- act

302 |   t2 <- currentTime

303 |   pure (v, t2 - t1)

305 | export %inline

306 | timed' : HasIO io => io () -> io Integer

307 | timed' = map snd . timed

310 | export %inline

311 | toClipboard : HasIO io => String -> io ()

312 | toClipboard s = primIO (prim__writeToClipboard s)

316 | itemToClipboard : Elem JSErr es => ClipboardItem -> Async JS es ()

317 | itemToClipboard ci = primIO (prim__itemToClipboard ci) >>= promise

320 | export %inline

321 | clipboardItem : HasIO io => (mimetype, content : String) -> io ClipboardItem

322 | clipboardItem m s = primIO (prim__clipboardItem m s)

326 | dataToClipboard : Elem JSErr es => (mimetype, content : String) -> Async JS es ()

327 | dataToClipboard m c = clipboardItem m c >>= itemToClipboard

330 | readFromClipboard1 : HasIO io => (String -> IO1 ()) -> io ()

331 | readFromClipboard1 cb = primIO $ prim__readFromClipboard (\s => primRun (cb s))

334 | readFromClipboard : Async e es String

335 | readFromClipboard =

336 |   primAsync_ $ \cb =>

337 |     ffi $ prim__readFromClipboard (\s => primRun (cb $ Right s))

340 | export %inline

341 | dialogShow : HasIO io => HTMLDialogElement -> io ()

342 | dialogShow el = primIO (prim__dialogShow el)

345 | export %inline

346 | dialogClose : HasIO io => HTMLDialogElement -> io ()

347 | dialogClose el = primIO (prim__dialogClose el)

350 | export %inline

351 | showModal : HasIO io => HTMLDialogElement -> io ()

352 | showModal el = primIO (prim__showModal el)

358 | public export

359 | interface ToBlob a where

360 |   toBlob : a -> AnyPtr

362 | export %inline

363 | ToBlob (IArray k String) where

364 |   toBlob = unsafeToPtr

366 | export %inline

367 | ToBlob (Indexed.Array String) where

368 |   toBlob (A _ arr) = toBlob arr

370 | export %inline

371 | ToBlob (List String) where

372 |   toBlob s = toBlob (arrayL s)

374 | export %inline

375 | ToBlob String where

376 |   toBlob s = toBlob $ array [s]

379 | blob : {0 a : _} -> HasIO io =>  ToBlob a => a -> (mimetype : String) -> io Blob

380 | blob v mimetype = primIO (prim__blob (toBlob v) mimetype)

386 | record ObjectURL where

387 |   constructor OU

388 |   url : String

390 | export %inline

391 | Resource (Async JS) ObjectURL where

392 |   cleanup (OU u) = primIO (prim__revokeObjectURL u)

394 | export %inline

395 | Cast ObjectURL String where cast = url

401 | export %inline

402 | blobURL : HasIO io => Blob -> io ObjectURL

403 | blobURL b = OU <$> primIO (prim__blobURL b)

405 | toAnyBuffer : Buffer -> AnyBuffer

406 | toAnyBuffer b = AB (cast $ prim__buflen b) (unsafeMakeBuffer b)

410 | blobBytes : Has JSErr es => Blob -> Async JS es AnyBuffer

411 | blobBytes b = primIO (prim__blobBytes b) >>= map toAnyBuffer . promise

418 | public export

419 | 0 ElemType : Ref t -> Type

420 | ElemType (Id _)   = Element

421 | ElemType (Elem _) = Element

422 | ElemType Body     = HTMLElement

423 | ElemType Document = Document

424 | ElemType Window   = Window

426 | public export

427 | 0 JS : List Type -> Type -> Type

428 | JS = Async JS

430 | nodeList : DocumentFragment -> List (HSum [Node,String])

431 | nodeList df = [inject $ df :> Node]

437 | parameters {auto has : Has JSErr es}

439 |   export %inline

440 |   js : JSIO t -> JS es t

441 |   js = injectIO . runEitherT

443 |   export

444 |   jsCast : SafeCast t => String -> s -> JS es t

445 |   jsCast msg = js . tryCast msg

447 |   export

448 |   unmaybe : Lazy String -> Maybe t -> JS es t

449 |   unmaybe msg = maybe (throw $ Caught msg) pure

451 |   export

452 |   body : JS es HTMLElement

453 |   body = getBody >>= unmaybe "document.body returned `Nothing`"

455 |   ||| Tries to retrieve an element of the given type by looking

460 |   export

461 |   getElementById : SafeCast t => Maybe String -> (id : String) -> JS es t

462 |   getElementById mtag id = do

463 |     e <- primIO (prim__getElementById id)

464 |     unmaybe msg $ nullableToMaybe e >>= castTo t

465 |     where

466 |       %inline tag, msg : String

467 |       tag = fromMaybe "element" mtag

468 |       msg = "getElementById: Could not find \{tag} with id \{id}"

470 |   ||| Tries to retrieve a HTMLElement by looking

474 |   export %inline

475 |   getHTMLElementById : (tag,id : String) -> JS es HTMLElement

476 |   getHTMLElementById = getElementById . Just

478 |   ||| Tries to retrieve an element of the given type by looking

483 |   export

484 |   getElementByRef : (r : Ref t) -> JS es (ElemType r)

485 |   getElementByRef (Id {tag} id) = getElementById (Just tag) id

486 |   getElementByRef (Elem id)     = getElementById Nothing id

487 |   getElementByRef Body          = body

488 |   getElementByRef Document      = document

489 |   getElementByRef Window        = window

491 |   err : String

492 |   err = "Web.Async.getElementByRef"

494 |   ||| Tries to retrieve an element of the given type by looking

499 |   export

500 |   castElementByRef : {0 x : k} -> SafeCast t => Ref x -> JS es t

501 |   castElementByRef ref = getElementByRef ref >>= jsCast err

503 |   ||| Sets a custom validity message at the given reference.

509 |   export %inline

510 |   validityMessage : Ref t -> (0 p : ValidityTag t) => String -> JS es ()

511 |   validityMessage r s =

512 |     castElementByRef r >>= \e => primIO (prim__setCustomValidity e s)

514 |   ||| Sets or unsets a custom validity message at the given node.

515 |   export

516 |   validate : Ref t -> (0 p : ValidityTag t) => Either String b -> JS es ()

517 |   validate r (Left s)  = validityMessage r s

518 |   validate r (Right s) = validityMessage r ""

520 |   ||| Sets the value of the element identified by the given ID.

524 |   export %inline

525 |   setValue : Ref t -> (0 p : ValueTag t) => String -> JS es ()

526 |   setValue r s = castElementByRef r >>= \e => primIO (prim__setValue e s)

532 | public export

533 | 0 Act : Type -> Type

534 | Act = Async JS [JSErr]

536 | public export

537 | 0 JSPull : Type -> Type -> Type

538 | JSPull o r = Pull (Async JS) o [JSErr] r

540 | public export

541 | 0 JSStream : Type -> Type

542 | JSStream o = Pull (Async JS) o [JSErr] ()

544 | export covering

545 | pullErr : AsyncStream f es Void -> Async f es ()

546 | pullErr s =

547 |   weakenErrors (pull s) >>= \case

548 |     Error err => fail err

549 |     _         => pure ()

551 | export covering %inline

552 | runJS : JS [JSErr] () -> IO ()

553 | runJS = app . handle [putStrLn . dispErr]

555 | export covering %inline

556 | runProg : JSStream Void -> IO ()

557 | runProg = runJS . pullErr

560 | mvcActEvs : JSStream e -> s -> (e -> s -> Act s) -> JSStream Void

561 | mvcActEvs evs ini act = evs |> P.evalScans1 ini (flip act) |> drain

563 | parameters (ev  : e)

564 |            (ini : s)

566 |   export

567 |   mvcAct : (Sink e => e -> s -> Act s) -> JSStream Void

568 |   mvcAct act = do

569 |     E evs <- exec $ eventFrom ev

570 |     mvcActEvs evs ini act

572 |   export

573 |   mvc : (e -> s -> s) -> (Sink e => e -> s -> Act ()) -> JSStream Void

574 |   mvc upd disp =

575 |     mvcAct (\v,x => let y := upd v x in disp v y $> y)

582 | getClientRect : LIO f => Element -> f Rect

583 | getClientRect el = Prelude.do

584 |   r <- lift1 $ ffi (prim__getBoundingClientRect el)

585 |   lift1 (toRect r)

591 | export %inline

592 | Resource (Async JS) Reader where

593 |   cleanup r = primIO (prim__cancelRead r)

596 | read : Elem JSErr es => Reader -> Async JS es (Maybe AnyBuffer)

597 | read r = Prelude.do

598 |   p <- primIO (prim__readChunk r) >>= promise

599 |   pure $ case prim__isDone p of

600 |     1 => Nothing

601 |     _ => Just $ toAnyBuffer (prim__buf p)