Web.MVC.Controller

Reexports

Definitions

0 Prog : Type -> Type -> Type -> Type

  A `Prog` controls some state of type `s` acting on events of
  type `e`.
  
  Based on an event and the current state, the controller produces a new
  state and a result (typically a command), which usually updates the
  UI in such a way that it can fire more events.

Totality: total
Visibility: public export

0 Controller : Type -> Type -> Type

Totality: total
Visibility: public export

(<$$>) : (x -> y) -> State s (Cmd x) -> State s (Cmd y)

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 4

map2 : (x -> y) -> State s (Cmd x) -> State s (Cmd y)

Totality: total
Visibility: export

direct : Monoid t => Prog e e t

  On an event, replaces the current state with the event's
  value without emitting a command.

Totality: total
Visibility: export

directM : Monoid t => Prog e (Maybe e) t

  Same as `direct` but for optional states.

Totality: total
Visibility: export

displayEv : (s -> Cmd t) -> Prog s s (Cmd t)

  A controller that replaces the state with the current event
  and display the new state.

Totality: total
Visibility: export

updateDisp : (e -> s -> s) -> (e -> s -> Cmd t) -> Prog e s (Cmd t)

  Update the state with the given function, the run a command
  derived from the new state.

Totality: total
Visibility: export

data Progs : List Type -> List Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : Progs [] []

(::) : Prog e s (Cmd e) -> Progs es ss -> Progs (e :: es) (s :: ss)

progs : Progs es ss -> Controller (HSum es) (HList ss)

  A list of controllers can be converted to a controller over
  a heterogeneous sum as the event type and a heterogeneous list
  as the state type.

Totality: total
Visibility: export

run : Prog e s (Cmd e) -> e -> s -> IO ()

Visibility: export

record Editor : Type -> Type -> Type -> Type -> Type

  An `Editor` describes how to "pop-up" new interactive DOM elements that
  typically serve as a form of (validated) user input. It consists of a
  `Controller` for the interactive element(s), but also describes an initial
  view to display and command to emit, based on the current state.
  
  An editor and its corresponding widgets can be something simple like a
  text input field or a `<select>` element, or it can be highly complex
  like a canvas and a group of DOM elements for editing molecules.
  
  Since an `Editor` describes a set of DOM elements that can potentially
  appear several times in a web page (for instance, when editing a list of
  values), its functions take a `DomID` as additional input, to distinguish
  between the different versions of the widget that are around.
  
  @i   : The ID type used to identify DOM elements
  
  @st  : The type used to internally store the current widget state
  
  @ev  : The event type the widget fires.
  
  @new : The type of data we can extract from the widget's internal state.

Totality: total
Visibility: public export
Constructor: 

E : (i -> Controller ev st) -> (i -> st -> Node ev) -> (i -> st -> Cmd ev) -> (st -> Either String new) -> (Maybe new -> st) -> Editor i st ev new

Projections:

.ctrl : Editor i st ev new -> i -> Controller ev st

  Update the inner state based on the current event.

.init : Editor i st ev new -> i -> st -> Cmd ev

  The initial command use to properly setup the view. This is used
  for initial validation or for drawing molecules to the canvas when
  editing starts. It is invoked after setting up the view.

.stToNew : Editor i st ev new -> st -> Either String new

  Try to convert the current state to a value of type `new` we can
  send to the server. This implements client-side validation, therefore,
  it returns an `Either`.

.toState : Editor i st ev new -> Maybe new -> st

  Create an initial state from an optional value of type `new`

.view : Editor i st ev new -> i -> st -> Node ev

  Create a widget from a unique identifier and the initial state.

.ctrl : Editor i st ev new -> i -> Controller ev st

  Update the inner state based on the current event.

Totality: total
Visibility: public export

ctrl : Editor i st ev new -> i -> Controller ev st

  Update the inner state based on the current event.

Totality: total
Visibility: public export

.view : Editor i st ev new -> i -> st -> Node ev

  Create a widget from a unique identifier and the initial state.

Totality: total
Visibility: public export

view : Editor i st ev new -> i -> st -> Node ev

  Create a widget from a unique identifier and the initial state.

Totality: total
Visibility: public export

.init : Editor i st ev new -> i -> st -> Cmd ev

  The initial command use to properly setup the view. This is used
  for initial validation or for drawing molecules to the canvas when
  editing starts. It is invoked after setting up the view.

Totality: total
Visibility: public export

init : Editor i st ev new -> i -> st -> Cmd ev

  The initial command use to properly setup the view. This is used
  for initial validation or for drawing molecules to the canvas when
  editing starts. It is invoked after setting up the view.

Totality: total
Visibility: public export

.stToNew : Editor i st ev new -> st -> Either String new

  Try to convert the current state to a value of type `new` we can
  send to the server. This implements client-side validation, therefore,
  it returns an `Either`.

Totality: total
Visibility: public export

stToNew : Editor i st ev new -> st -> Either String new

  Try to convert the current state to a value of type `new` we can
  send to the server. This implements client-side validation, therefore,
  it returns an `Either`.

Totality: total
Visibility: public export

.toState : Editor i st ev new -> Maybe new -> st

  Create an initial state from an optional value of type `new`

Totality: total
Visibility: public export

toState : Editor i st ev new -> Maybe new -> st

  Create an initial state from an optional value of type `new`

Totality: total
Visibility: public export

newIso : Iso' n1 n2 -> Editor i st ev n1 -> Editor i st ev n2

  View an editor through an isomorphism.

Totality: total
Visibility: export

noInit : i -> s -> Cmd e

  Utility for editors without initial command.

Totality: total
Visibility: export

toNewM : Editor i st ev new -> Maybe st -> Maybe new

  Tries to convert the current (optional) state of an editor to
  an updated value.

Totality: total
Visibility: export

newP : Prism' t s -> Editor i st ev s -> Editor i st ev t

  Views the `new` values of an editor through a prism.

Totality: total
Visibility: export

dummy : n -> Editor i () Void n

  A dummy `Editor` for uneditable values.

Totality: total
Visibility: public export

elemChildren : Cast t DomID => t -> List (Node e) -> Cmd e

Totality: total
Visibility: export

elemChild : Cast t DomID => t -> Node e -> Cmd e

Totality: total
Visibility: export

elemAppend : Cast t DomID => t -> Node e -> Cmd e

Totality: total
Visibility: export

elemPrepend : Cast t DomID => t -> Node e -> Cmd e

Totality: total
Visibility: export

clearElem : Cast t DomID => t -> Cmd e

Totality: total
Visibility: export

removeElem : Cast t DomID => t -> Cmd e

Totality: total
Visibility: export

replaceElem : Cast t DomID => t -> Node e -> Cmd e

Totality: total
Visibility: export

btnAttr : Cast t DomID => t -> Attribute Button e -> Cmd e

Totality: total
Visibility: export