Text.HTML.Validation

Definitions

record ValEnv : Type -> Type

  Environment for validating editable componends

Totality: total
Visibility: public export
Constructor: 

VE : (i -> i) -> (i -> i) -> Class -> Class -> String -> ValEnv i

Projections:

.inputID : ValEnv i -> i -> i

  DOM ID for `<input>` fields based on a parent ID

.mandatory : ValEnv i -> String

  String for mandatory fields. This is used with validated `<input>`
  fields, when they contain only empty (invalid) input.

.msgCls : ValEnv i -> Class

  Class used for the component display the validation message

.msgID : ValEnv i -> i -> i

  DOM ID for validation message elements based on a parent ID

.widgetCls : ValEnv i -> Class

  Class used for the component display the validated widget

.inputID : ValEnv i -> i -> i

  DOM ID for `<input>` fields based on a parent ID

Totality: total
Visibility: public export

inputID : ValEnv i -> i -> i

  DOM ID for `<input>` fields based on a parent ID

Totality: total
Visibility: public export

.msgID : ValEnv i -> i -> i

  DOM ID for validation message elements based on a parent ID

Totality: total
Visibility: public export

msgID : ValEnv i -> i -> i

  DOM ID for validation message elements based on a parent ID

Totality: total
Visibility: public export

.widgetCls : ValEnv i -> Class

  Class used for the component display the validated widget

Totality: total
Visibility: public export

widgetCls : ValEnv i -> Class

  Class used for the component display the validated widget

Totality: total
Visibility: public export

.msgCls : ValEnv i -> Class

  Class used for the component display the validation message

Totality: total
Visibility: public export

msgCls : ValEnv i -> Class

  Class used for the component display the validation message

Totality: total
Visibility: public export

.mandatory : ValEnv i -> String

  String for mandatory fields. This is used with validated `<input>`
  fields, when they contain only empty (invalid) input.

Totality: total
Visibility: public export

mandatory : ValEnv i -> String

  String for mandatory fields. This is used with validated `<input>`
  fields, when they contain only empty (invalid) input.

Totality: total
Visibility: public export

validated : Cast i DomID => ValEnv i => i -> Node e -> Node e

  Pairs a widget with an element where validation messages can be
  displayed.

Totality: total
Visibility: export

vinp : Cast i DomID => ValEnv i => Class -> InputType -> i -> String -> Node String

  A validated text field.

Totality: total
Visibility: export