Web.MVC.Animate

Utilities not (yet) available from idris2-dom

Definitions

currentTime : HasIO io => io Integer

  Get the current time in milliseconds since 1970/01/01.

Visibility: export

timed : (Integer -> e) -> Cmd e -> Cmd e

  Determine the time taken to setup a command and wrap it in an
  event that will be fired synchronously.

Visibility: export

data IntervalID : Type

  ID used to identify and cancel a running timer.

Totality: total
Visibility: public export

every : e -> Bits32 -> Cmd e

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

Visibility: export

everyWithCleanup : (IO () -> e) -> e -> Bits32 -> Cmd e

  Fires the given event every `n` milliseconds.
  
  In addition, this synchronously fires an event with a wrapped
  handle for stopping the timer.

Visibility: export

DTime : Type

  Alias for a time delta in milliseconds

Visibility: public export

animate : (DTime -> e) -> Cmd e

  Repeatedly fires the given event holding the time delta in
  milliseconds since the last animation step.

Visibility: export

animateWithCleanup : (IO () -> e) -> (DTime -> e) -> Cmd e

  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