Web.Async.Animate

Utilities not (yet) available from idris2-dom

Definitions

data IntervalID : Type

  ID used to identify and cancel a running timer.

Totality: total
Visibility: public export

every : Sink e => e -> Bits32 -> IO1 (IO1 ())

  Fires the given event every `n` milliseconds.
  
  Note: Use `animate` for smoothly running animations.

Visibility: export

DTime : Type

  Alias for a time delta in milliseconds

Visibility: public export

animate : Sink e => (DTime -> e) -> IO1 (IO1 ())

  Repeatedly fires the given event holding the time delta in
  milliseconds since the last animation step.
  
  In addition, synchronously fires an event with a wrapped
  handle for stopping the animation.

Visibility: export