0 | module Web.MVC.Controller.Validation
 1 |
 2 | import Data.String
 3 | import Text.HTML.Extra
 4 | import Web.MVC
 5 | import Web.MVC.Controller
 6 |
 7 | %default total
 8 |
 9 | parameters {0      i : Type}
10 |            {auto cst : Cast i DomID}
11 |            {auto env : ValEnv i}
12 |
13 |   ||| Sets the associated validation text of a validated widget based on
14 |   ||| its current state.
15 |   export
16 |   validateState : (s -> Either String t) -> i -> s -> Cmd e
17 |   validateState f u = elemChild (env.msgID u) . Text . either id (const "") . f
18 |
19 |   ||| Sets the validation message of an `<input>` element based on its
20 |   ||| current value.
21 |   export
22 |   valTextInput : (String -> Either String t) -> i -> Controller String String
23 |   valTextInput rd u = displayEv (validate (inpRef $ env.inputID u) . rd)
24 |
25 |   ||| Converts an editor representing an interactive widget to one
26 |   ||| with an associated DOM element for displaying validation text
27 |   ||| messages.
28 |   export
29 |   validated : Editor i s e n -> Editor i s e n
30 |   validated ed =
31 |     E (\u,v => ed.ctrl u v <+> map (validateState ed.stToNew u) get)
32 |       (\u,s => validated u (ed.view u s))
33 |       (\u,s => validateState ed.stToNew u s <+> ed.init u s)
34 |       ed.stToNew
35 |       ed.toState
36 |
37 |   export
38 |   checkVal : (String -> Either String t) -> String -> Either String t
39 |   checkVal f s =
40 |     case f s of
41 |       Right v => Right v
42 |       Left  x => if trim s == "" then Left env.mandatory else Left x
43 |
44 |   ||| An editor for editing values as strings via `<input>` elements.
45 |   |||
46 |   ||| @cls : CSS class for the input text field we use.
47 |   |||
48 |   ||| @tpe : Type of the input field
49 |   |||
50 |   ||| @rd  : Reading function for converting strings to values of the
51 |   |||        desired type
52 |   |||
53 |   ||| @disp : Function for displaying client-side values.
54 |   |||
55 |   ||| @ini  : Initial (client-side) value
56 |   export %inline
57 |   input :
58 |        (cls     : Class)
59 |     -> (tpe     : InputType)
60 |     -> (stToNew : String -> Either String new)
61 |     -> (disp    : Maybe new -> String)
62 |     -> Editor i String String new
63 |   input c tpe f =
64 |     let g := checkVal f in E (valTextInput g) (vinp c tpe) noInit g
65 |