Web.MVC.Widget

Definitions

record Widget : Type

  A `Widget` is a standalone UI element that manages its own
  state. It packages up all aspects of an MVC component into a
  single piece of data that can be passed around and transformed,
  before finally turned into a runnable program with `runWidget`.
  
  See the various parameters of `Web.MVC.runMVC` for further
  explanation.

Totality: total
Visibility: public export
Constructor: 

MkWidget : (0 St : Type) -> (0 Ev : Type) -> St -> (St -> Cmd Ev) -> (Ev -> St -> St) -> (Ev -> St -> Cmd Ev) -> Widget

Projections:

0 .Ev : Widget -> Type

  Event type

0 .St : Widget -> Type

  The internal state of the widget (model)

.display : ({rec:0} : Widget) -> Ev {rec:0} -> St {rec:0} -> Cmd (Ev {rec:0})

  Update the UI based on the latest event and the current state

.init : ({rec:0} : Widget) -> St {rec:0}

  Initial state

.setup : ({rec:0} : Widget) -> St {rec:0} -> Cmd (Ev {rec:0})

  Given the initial state, set up the  UI

.update : ({rec:0} : Widget) -> Ev {rec:0} -> St {rec:0} -> St {rec:0}

  Update the state based on the latest event

Hints:

Monoid Widget

Semigroup Widget

0 .St : Widget -> Type

  The internal state of the widget (model)

Totality: total
Visibility: public export

0 St : Widget -> Type

  The internal state of the widget (model)

Totality: total
Visibility: public export

0 .Ev : Widget -> Type

  Event type

Totality: total
Visibility: public export

0 Ev : Widget -> Type

  Event type

Totality: total
Visibility: public export

.init : ({rec:0} : Widget) -> St {rec:0}

  Initial state

Totality: total
Visibility: public export

init : ({rec:0} : Widget) -> St {rec:0}

  Initial state

Totality: total
Visibility: public export

.setup : ({rec:0} : Widget) -> St {rec:0} -> Cmd (Ev {rec:0})

  Given the initial state, set up the  UI

Totality: total
Visibility: public export

setup : ({rec:0} : Widget) -> St {rec:0} -> Cmd (Ev {rec:0})

  Given the initial state, set up the  UI

Totality: total
Visibility: public export

.update : ({rec:0} : Widget) -> Ev {rec:0} -> St {rec:0} -> St {rec:0}

  Update the state based on the latest event

Totality: total
Visibility: public export

update : ({rec:0} : Widget) -> Ev {rec:0} -> St {rec:0} -> St {rec:0}

  Update the state based on the latest event

Totality: total
Visibility: public export

.display : ({rec:0} : Widget) -> Ev {rec:0} -> St {rec:0} -> Cmd (Ev {rec:0})

  Update the UI based on the latest event and the current state

Totality: total
Visibility: public export

display : ({rec:0} : Widget) -> Ev {rec:0} -> St {rec:0} -> Cmd (Ev {rec:0})

  Update the UI based on the latest event and the current state

Totality: total
Visibility: public export

runWidget : (JSErr -> IO ()) -> Widget -> IO ()

  Run a `Widget`. This is basically `runMVC` with the arguments
  constructed from the fields of `Widget`. Since this function
  produces no result, there's no going back from here: all `Widget`
  composition and transformation must be done beforehand.

Visibility: export