Idris2Doc : Web.Async.Form

Web.Async.Form

(source)

Reexports

import public Control.Barbie
import public Data.Singleton
import public Monocle
import public Web.Async
import public Web.Async.Widget

Definitions

record FormField : Type
  An editable field in a web form consisting of the field's
name, the node for data input, and an ID that will be used
to send validation messages to a label.

Totality: total
Visibility: public export
Constructor: 
FF : String -> HTMLNodes -> FormField

Projections:
.name : FormField -> String
.nodes : FormField -> HTMLNodes
.name : FormField -> String
Totality: total
Visibility: public export
name : FormField -> String
Totality: total
Visibility: public export
.nodes : FormField -> HTMLNodes
Totality: total
Visibility: public export
nodes : FormField -> HTMLNodes
Totality: total
Visibility: public export
form : DOMLocal => Interpolation f => (0 rec : ((f -> Type) -> Type)) -> (FormField -> HTMLNode) -> rec Singleton => FunctorB f rec => ApplicativeB f rec => TraversableB f rec => RecordB f rec => rec (Editor . g) -> Editor (rec g)
  An editable web form where the different fields of a
record can be edited and validated.

The record in question must be a *barbie*
(see the corresponding library), and this function takes as
input such a record of editors and returns an editor of
the record.

@ `rec` : the barbie record type used to group the
field values.
@ `formNode` : used to group and display the different
form fields in a single HTML node.

Note: For uneditable record fields that should not appear in the
user interface, use a `dummy` editor.

Totality: total
Visibility: export
hform : DOMLocal => All (\{arg:0} => Elem {arg:0} ts) ts => All Editor ts -> Editor (HList ts)
  An editable web form where the different fields of a
record can be edited and validated.

The record in question must be a *barbie*
(see the corresponding library), and this function takes as
input such a record of editors and returns an editor of
the record.

@ `rec` : the barbie record type used to group the
field values.

Note: For uneditable record fields that should not appear in the
user interface, use a `dummy` editor.

Totality: total
Visibility: export