Web.Async.Form

Reexports

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 -> HTMLNode -> FormField

Projections:

.name : FormField -> String

.node : FormField -> HTMLNode

.name : FormField -> String

Totality: total
Visibility: public export

name : FormField -> String

Totality: total
Visibility: public export

.node : FormField -> HTMLNode

Totality: total
Visibility: public export

node : FormField -> HTMLNode

Totality: total
Visibility: public export

form : Interpolation f => (0 rec : ((f -> Type) -> Type)) -> (List 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 : (List HTMLNode -> HTMLNode) -> 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.
  @ `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