Web.Async.Widget.Types

Definitions

data EditRes : Type -> Type

  Result of editing some kind of input element.
  
  Input is either missing, invalid, or valid.

Totality: total
Visibility: public export
Constructors:

Missing : EditRes t

Invalid : String -> EditRes t

Valid : t -> EditRes t

Hints:

Applicative EditRes

Eq {arg:3573} => Eq (EditRes {arg:3573})

Functor EditRes

Monad EditRes

Show {arg:3573} => Show (EditRes {arg:3573})

toEither : EditRes t -> Either String ()

Totality: total
Visibility: export

toMaybe : EditRes t -> Maybe t

Totality: total
Visibility: export

isValid : EditRes t -> Bool

Totality: total
Visibility: export

validity : EditRes s -> Attribute t

Totality: total
Visibility: export

record Widget : Type -> Type

  A `Widget e` is an interactive UI element that emits
  events of type `e`.

Totality: total
Visibility: public export
Constructor: 

W : HTMLNodes -> JSStream e -> Widget e

Projections:

.events : Widget e -> JSStream e

.nodes : Widget e -> HTMLNodes

Hint: 

Functor Widget

.nodes : Widget e -> HTMLNodes

Totality: total
Visibility: public export

nodes : Widget e -> HTMLNodes

Totality: total
Visibility: public export

.events : Widget e -> JSStream e

Totality: total
Visibility: public export

events : Widget e -> JSStream e

Totality: total
Visibility: public export

adjNodes : (HTMLNodes -> HTMLNodes) -> Widget e -> Widget e

Totality: total
Visibility: export

constant : t -> Widget t

  A dummy widget without a node representation that keeps
  producing the given value.

Totality: total
Visibility: export

empty : Widget t

  A dummy widget without a node representation that
  never fires an event.

Totality: total
Visibility: export

once : t -> Widget t

  A dummy widget without a node representation that
  fires the given event exactly once.

Totality: total
Visibility: export

record FileEv : Type

Totality: total
Visibility: public export
Constructor: 

FE : File -> String -> FileEv

Projections:

.file : FileEv -> File

.name : FileEv -> String

Hint: 

Interpolation FileEv

.file : FileEv -> File

Totality: total
Visibility: public export

file : FileEv -> File

Totality: total
Visibility: public export

.name : FileEv -> String

Totality: total
Visibility: public export

name : FileEv -> String

Totality: total
Visibility: public export

map2 : Functor f => Functor g => (x -> y) -> f (g x) -> f (g y)

Totality: total
Visibility: export

map3 : Functor f => Functor g => Functor h => (x -> y) -> f (g (h x)) -> f (g (h y))

Totality: total
Visibility: export

record Editor : Type -> Type

  An `Editor` describes how to create new interactive DOM elements that
  typically serve as a form of (validated) user input. It consists of an
  `HTMLNode` for displaying the editing form plus a stream of validated
  input data.
  
  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.
  
  A couple of notes about how an editor is supposed to behave:
    * If the initial value used for creating the widget is a `Nothing`,
      the stream of values produced by the widget *may* already hold
      a valid default value. In case no sensible default is available,
      the stream's initial value *should* be `Missing`.
    * If the initial value used for creating the widget is a `Just`,
      the stream of values produced by the widget *must* emit a `Valid`
      wrapping the provided initial value as its first output.
  
  The above two rules make sure an editor behaves as expected, especially
  when combining several editors in a form, or using the experimental
  `bindEd` combinator.

Totality: total
Visibility: public export
Constructor: 

E : (Maybe t -> Act (Widget (EditRes t))) -> Editor t

Projection: 

.widget : Editor t -> Maybe t -> Act (Widget (EditRes t))

  Create a node and stream of values from an optional initial value.

.widget : Editor t -> Maybe t -> Act (Widget (EditRes t))

  Create a node and stream of values from an optional initial value.

Totality: total
Visibility: public export

widget : Editor t -> Maybe t -> Act (Widget (EditRes t))

  Create a node and stream of values from an optional initial value.

Totality: total
Visibility: public export

adjWidget : (Maybe a -> Maybe b) -> (Widget (EditRes b) -> Widget (EditRes a)) -> Editor b -> Editor a

Totality: total
Visibility: export

edNodes : (HTMLNodes -> HTMLNodes) -> Editor t -> Editor t

Totality: total
Visibility: export

adjEditor : (Maybe a -> Maybe b) -> (EditRes b -> EditRes a) -> Editor b -> Editor a

Totality: total
Visibility: export

editI : Iso' t1 t2 -> Editor t1 -> Editor t2

  Views an editor through an isomorphism.

Totality: total
Visibility: export

editP : Prism' t2 t1 -> Editor t1 -> Editor t2

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

Totality: total
Visibility: export

refineEdit : (t2 -> Maybe t1) -> (t1 -> EditRes t2) -> Editor t1 -> Editor t2

  Refines an editor to produce values of a more restricted type.

Totality: total
Visibility: export

mapEvents : (JSStream (EditRes t) -> JSStream (EditRes t)) -> Editor t -> Editor t

Totality: total
Visibility: export

dummy : t -> Editor t

  A dummy `Editor` for uneditable values.
  
  The given value is fired exactly once.

Totality: total
Visibility: public export