0 | ||| Utilities not (yet) available from idris2-dom
 1 | module Web.Async.Animate
 2 |
 3 | import Data.Linear.Token
 4 | import JS
 5 | import Syntax.T1
 6 | import Web.Async.Util
 7 |
 8 | --------------------------------------------------------------------------------
 9 | --          Timers
10 | --------------------------------------------------------------------------------
11 |
12 | ||| ID used to identify and cancel a running timer.
13 | public export
14 | data IntervalID : Type where [external]
15 |
16 | %foreign "browser:lambda:(n,h,w)=>setInterval(() => h(w),n)"
17 | prim__setInterval : Bits32 -> PrimIO () -> PrimIO IntervalID
18 |
19 | %foreign "browser:lambda:(i,w)=>clearInterval(i)"
20 | prim__clearInterval : IntervalID -> PrimIO ()
21 |
22 | ||| Fires the given event every `n` milliseconds.
23 | |||
24 | ||| Note: Use `animate` for smoothly running animations.
25 | export
26 | every : (s : Sink e) => e -> (n : Bits32) -> IO1 (IO1 ())
27 | every ev millis t =
28 |   let i # t := ffi (prim__setInterval millis (primRun $ s.sink1 ev)) t
29 |    in ffi (prim__clearInterval i) # t
30 |
31 | --------------------------------------------------------------------------------
32 | --          Animations
33 | --------------------------------------------------------------------------------
34 |
35 | %foreign """
36 |          browser:lambda:(cont,h,w)=>{
37 |             let previousTimeStamp;
38 |
39 |             function step(timestamp) {
40 |               if (previousTimeStamp === undefined)
41 |                 previousTimeStamp = timestamp;
42 |               const dtime = timestamp - previousTimeStamp;
43 |               previousTimeStamp = timestamp;
44 |               if (cont(w)) {
45 |                 h(dtime)(w)
46 |                 window.requestAnimationFrame(step);
47 |               }
48 |             }
49 |
50 |             window.requestAnimationFrame(step);
51 |          }
52 |          """
53 | prim__animate : PrimIO Boolean -> (Bits32 -> PrimIO ()) -> PrimIO ()
54 |
55 | ||| Alias for a time delta in milliseconds
56 | public export
57 | DTime : Type
58 | DTime = Bits32
59 |
60 | ||| Repeatedly fires the given event holding the time delta in
61 | ||| milliseconds since the last animation step.
62 | |||
63 | ||| In addition, synchronously fires an event with a wrapped
64 | ||| handle for stopping the animation.
65 | export
66 | animate : (s : Sink e) => (DTime -> e) -> IO1 (IO1 ())
67 | animate ev = T1.do
68 |   ref <- ref1 true
69 |   ffi (prim__animate (primRun $ read1 ref) (primRun . s.sink1 . ev))
70 |   pure $ write1 ref false
71 |