0 | ||| Utilities for working with `<select>` elements
 1 | module Text.HTML.Select
 2 |
 3 | import Data.List
 4 | import Data.Nat
 5 | import Text.HTML
 6 |
 7 | %default total
 8 |
 9 | public export
10 | data SelectEntry : (t : Type) -> Type where
11 |   Title : String    -> SelectEntry t
12 |   Entry : (val : t) -> String -> SelectEntry t
13 |
14 | --------------------------------------------------------------------------------
15 | -- Utilities
16 | --------------------------------------------------------------------------------
17 |
18 | ix : List (SelectEntry t) -> Nat -> Maybe t
19 | ix []                _     = Nothing
20 | ix (Entry v _ :: xs) 0     = Just v
21 | ix (Title s   :: xs) 0     = Nothing
22 | ix (x :: xs)         (S k) = ix xs k
23 |
24 | app : {0 a : _} -> SnocList (a,List b) -> SnocList b -> a -> SnocList (a,List b)
25 | app sx [<] x = sx
26 | app sx sy  x = sx :< (x, sy <>> [])
27 |
28 | groups :
29 |      SnocList (String,List (Nat,t,String))
30 |   -> SnocList (Nat,t,String)
31 |   -> (lbl : String)
32 |   -> Nat
33 |   -> List (SelectEntry t)
34 |   -> List (String,List (Nat,t,String))
35 | groups sg sp l n []                = app sg sp l <>> []
36 | groups sg sp l n (Title s   :: xs) = groups (app sg sp l) [<]  s (S n) xs
37 | groups sg sp l n (Entry v s :: xs) = groups sg (sp :< (n,v,s)) l (S n) xs
38 |
39 | export
40 | selectEntries :
41 |      (entries : List (SelectEntry t))
42 |   -> (sel     : t -> Bool)
43 |   -> (toEvent : t -> e)
44 |   -> (attrs   : List (Attribute Select e))
45 |   -> Node e
46 | selectEntries es sel toEv attrs =
47 |   select
48 |     -- Note: The `change` event handler must be the last attribute
49 |     --       otherwise it might already fire when the node is being
50 |     --       set up.
51 |     (attrs ++ [onChangeMaybe (map toEv . ix es . cast)])
52 |     (groups [<] [<] "" 0 es >>= grp)
53 |   where
54 |     opt : (Nat,t,String) -> Node e
55 |     opt (x,v,s) = option [value (show x), selected (sel v)] [Text s]
56 |
57 |     grp : (String,List (Nat,t,String)) -> List (Node e)
58 |     grp ("",ps) = map opt ps
59 |     grp (s,ps)  = [optgroup [label s] $ map opt ps]
60 |
61 | ||| Create a `<select>` element displaying the options in the given
62 | ||| list.
63 | |||
64 | ||| @values  : the list of options
65 | ||| @sel     : true if the given item in the list should be selected
66 | ||| @display : how to display an option at the UI
67 | ||| @toEvent : how to convert an option to an event
68 | ||| @attrs   : additional attributes
69 | export
70 | selectFromListBy :
71 |      (values  : List t)
72 |   -> (sel     : t -> Bool)
73 |   -> (display : t -> String)
74 |   -> (toEvent : t -> e)
75 |   -> (attrs   : List (Attribute Select e))
76 |   -> Node e
77 | selectFromListBy vs sel f = selectEntries ((\x => Entry x $ f x) <$> vs) sel
78 |
79 | ||| Like `selectFromListBy` but uses an optional initial value
80 | ||| to determine the initially selected value.
81 | |||
82 | ||| @values  : the list of options
83 | ||| @init    : the initially selected option (if any)
84 | ||| @display : how to display an option at the UI
85 | ||| @toEvent : how to convert an option to an event
86 | ||| @attrs   : additional attributes
87 | export
88 | selectFromList :
89 |      {auto eq : Eq t}
90 |   -> (values  : List t)
91 |   -> (init    : Maybe t)
92 |   -> (display : t -> String)
93 |   -> (toEvent : t -> e)
94 |   -> (attrs   : List (Attribute Select e))
95 |   -> Node e
96 | selectFromList vs i = selectFromListBy vs ((i ==) . Just)
97 |