
  0 | module Text.HTML.Validation
  1 | 
  2 | import Text.HTML
  3 | import Text.HTML.Class
  4 | import Text.HTML.DomID
  5 | 
  6 | %default total
  7 | 
  8 | ||| Environment for validating editable componends
  9 | public export
 10 | record ValEnv (i : Type) where
 11 |   [noHints]
 12 |   constructor VE
 13 | 
 14 |   ||| DOM ID for `<input>` fields based on a parent ID
 15 |   inputID   : i -> i
 16 | 
 17 |   ||| DOM ID for validation message elements based on a parent ID
 18 |   msgID     : i -> i
 19 | 
 20 |   ||| Class used for the component display the validated widget
 21 |   widgetCls : Class
 22 | 
 23 |   ||| Class used for the component display the validation message
 24 |   msgCls    : Class
 25 | 
 26 |   ||| String for mandatory fields. This is used with validated `<input>`
 27 |   ||| fields, when they contain only empty (invalid) input.
 28 |   mandatory : String
 29 | 
 30 | parameters {0      i : Type}
 31 |            {auto cst : Cast i DomID}
 32 |            {auto env : ValEnv i}
 33 | 
 34 |   ||| Pairs a widget with an element where validation messages can be
 35 |   ||| displayed.
 36 |   export
 37 |   validated : i -> Node e -> Node e
 38 |   validated _ Empty = Empty
 39 |   validated u n     =
 40 |     cell env.widgetCls [] [n, cell env.msgCls [ref (env.msgID u)] []]
 41 | 
 42 |   ||| A validated text field.
 43 |   export
 44 |   vinp : Class -> (tpe : InputType) -> i -> String -> Node String
 45 |   vinp c tpe u v = inp c id [value v, ref $ env.inputID u, type tpe]
 46 |