Web.Async.Widget

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

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 : HTMLNode -> JSStream e -> Widget e

Projections:

.events : Widget e -> JSStream e

.node : Widget e -> HTMLNode

Hint: 

Functor Widget

.node : Widget e -> HTMLNode

Totality: total
Visibility: public export

node : Widget e -> HTMLNode

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

adjNode : (HTMLNode -> HTMLNode) -> 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

endOnRemove : Widget t -> JS es (Widget t)

  Adjusts a widget in such a way that its input streams ends
  as soon as its node is removed from the DOM.
  
  This is used in utilities such as `bindEd` or `Web.Async.List`, where
  external events decide when a node is removed from the UI.

Totality: total
Visibility: export

disabledEdit : Has JSErr es => Ref t -> EditRes a -> JS es ()

  Sets the `disabled` attribute of the given element
  if the given values is not a `Valid`.
  
  This is useful for disabling components such as buttons
  in the UI in case of invalid user input.

Totality: total
Visibility: export

voidRef : Ref t -> Ref Void

Totality: total
Visibility: export

attributesWithID : LIO io => (0 t : HTMLTag s) -> List (Attribute t) -> io (Ref t, List (Attribute t))

  Adds a unique ID to the given list of attributes if it does not yet
  already have an ID attribute, and returns the updated list plus the ID.

Totality: total
Visibility: export

nodeWithID : LIO io => HTMLNode -> io (Maybe (Ref Void, HTMLNode))

  Adds a unique ID to the given HTML node if it does not yet
  already have an ID and returns the updated node plus its ID.
  
  Returns `Nothing` in case the node in question is a `Raw` node
  or a `Text` node.

Totality: total
Visibility: export

textIn : InputType -> List (Attribute Input) -> String -> JS es (Widget String)

  An input element that emits `String` events.

Totality: total
Visibility: export

valIn : InputType -> List (Attribute Input) -> String -> (String -> EditRes e) -> JS es (Widget (EditRes e))

  A validated input element that emits events of type
  `EditRes e`.
  
  A custom validity message is set in case of invalid input.

Totality: total
Visibility: export

record FileEv : Type

Totality: total
Visibility: public export
Constructor: 

FE : File -> String -> FileEv

Projections:

.file : FileEv -> File

.name : FileEv -> String

.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

onFileIn : Sink e => (FileEv -> e) -> Attribute Input

Totality: total
Visibility: export

fileIn : Attributes Input -> JS es (Widget (EditRes FileEv))

Totality: total
Visibility: export

sel : Eq t => (v -> t) -> (v -> String) -> List v -> List (Attribute Select) -> Maybe t -> JS es (Widget (EditRes t))

  A select element displaying the values of type `v`
  shown in the given list.
  
  It fires events of type `t`, and uses two functions, one for
  converting elements to events and one for displaying elements.

Totality: total
Visibility: export

selEntries : Eq t => List (SelectEntry t) -> List (Attribute Select) -> Maybe t -> JS es (Widget (EditRes t))

  A select element displaying the values of type `v`
  shown in the given list.
  
  It fires events of type `t`, and uses two functions, one for
  converting elements to events and one for displaying elements.

Totality: total
Visibility: 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

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

txtEdit : (String -> EditRes t) -> InputType -> (Maybe t -> String) -> List (Attribute Input) -> Editor t

Totality: total
Visibility: export

selEdit : Interpolation t => Eq t => List t -> List (Attribute Select) -> Editor t

Totality: total
Visibility: export

bindEd : Class -> (HTMLNode -> HTMLNode -> HTMLNode) -> (a -> Editor b) -> (Maybe b -> a) -> Editor a -> Editor b

Totality: total
Visibility: export