0 | module Text.HTML.Select
  1 |
  2 | import Data.List
  3 | import Data.Nat
  4 | import FS.Concurrent.Signal
  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 | public export
 15 | record SelectEv t where
 16 |   constructor SE
 17 |   index : Nat
 18 |   label : String
 19 |   value : t
 20 |
 21 | export
 22 | Functor SelectEv where
 23 |   map f (SE i l v) = SE i l $ f v
 24 |
 25 | --------------------------------------------------------------------------------
 26 | -- Utilities
 27 | --------------------------------------------------------------------------------
 28 |
 29 | selectIx : List (SelectEntry t) -> Nat -> Maybe (SelectEv t)
 30 | selectIx vs n = go vs n
 31 |   where
 32 |     go : List (SelectEntry t) -> Nat -> Maybe (SelectEv t)
 33 |     go []                _     = Nothing
 34 |     go (Entry v s :: xs) 0     = Just (SE n s v)
 35 |     go (Title _   :: xs) 0     = Nothing
 36 |     go (x :: xs)         (S k) = go xs k
 37 |
 38 | app : {0 a : _} -> SnocList (a,List b) -> SnocList b -> a -> SnocList (a,List b)
 39 | app sx [<] x = sx
 40 | app sx sy  x = sx :< (x, sy <>> [])
 41 |
 42 | groups :
 43 |      SnocList (String,List (Nat,t,String))
 44 |   -> SnocList (Nat,t,String)
 45 |   -> (lbl : String)
 46 |   -> Nat
 47 |   -> List (SelectEntry t)
 48 |   -> List (String,List (Nat,t,String))
 49 | groups sg sp l n []                = app sg sp l <>> []
 50 | groups sg sp l n (Title s   :: xs) = groups (app sg sp l) [<]  s (S n) xs
 51 | groups sg sp l n (Entry v s :: xs) = groups sg (sp :< (n,v,s)) l (S n) xs
 52 |
 53 | export
 54 | selectEntries :
 55 |      {auto snk : Sink (SelectEv e)}
 56 |   -> (entries  : List (SelectEntry t))
 57 |   -> (sel      : t -> Bool)
 58 |   -> (toEvent  : t -> e)
 59 |   -> (attrs    : List (Attribute Select))
 60 |   -> HTMLNode
 61 | selectEntries es sel toEv attrs =
 62 |   select
 63 |     -- Note: The `change` event handler must be the last attribute
 64 |     --       otherwise it might already fire when the node is being
 65 |     --       set up.
 66 |     (attrs ++ [onChangeMaybe (map (map toEv) . selectIx es . cast)])
 67 |     (groups [<] [<] "" 0 es >>= grp)
 68 |   where
 69 |     opt : (Nat,t,String) -> HTMLNode
 70 |     opt (x,v,s) = option [value (show x), selected (sel v)] [Text s]
 71 |
 72 |     grp : (String,List (Nat,t,String)) -> HTMLNodes
 73 |     grp ("",ps) = map opt ps
 74 |     grp (s,ps)  = [optgroup [label s] $ map opt ps]
 75 |
 76 | ||| Create a `<select>` element displaying the options in the given
 77 | ||| list.
 78 | |||
 79 | ||| @values  : the list of options
 80 | ||| @sel     : true if the given item in the list should be selected
 81 | ||| @display : how to display an option at the UI
 82 | ||| @toEvent : how to convert an option to an event
 83 | ||| @attrs   : additional attributes
 84 | export
 85 | selectFromListBy :
 86 |      {auto snk : Sink (SelectEv e)}
 87 |   -> (values   : List t)
 88 |   -> (sel      : t -> Bool)
 89 |   -> (display  : t -> String)
 90 |   -> (toEvent  : t -> e)
 91 |   -> (attrs    : List (Attribute Select))
 92 |   -> HTMLNode
 93 | selectFromListBy vs sel f = selectEntries ((\x => Entry x $ f x) <$> vs) sel
 94 |
 95 | ||| Like `selectFromListBy` but uses an optional initial value
 96 | ||| to determine the initially selected value.
 97 | |||
 98 | ||| @values  : the list of options
 99 | ||| @init    : the initially selected option (if any)
100 | ||| @display : how to display an option at the UI
101 | ||| @toEvent : how to convert an option to an event
102 | ||| @attrs   : additional attributes
103 | export
104 | selectFromList :
105 |      {auto snk : Sink (SelectEv e)}
106 |   -> {auto eq : Eq t}
107 |   -> (values  : List t)
108 |   -> (init    : Maybe t)
109 |   -> (display : t -> String)
110 |   -> (toEvent : t -> e)
111 |   -> (attrs   : List (Attribute Select))
112 |   -> HTMLNode
113 | selectFromList vs i = selectFromListBy vs ((i ==) . Just)
114 |
115 | parameters {auto snk : Sink e}
116 |
117 |   ||| Simplified version of `selectEntries` that does not take
118 |   ||| a full `SelectEvent` sink.
119 |   export %inline
120 |   selectEntries' :
121 |        (entries  : List (SelectEntry t))
122 |     -> (sel      : t -> Bool)
123 |     -> (toEvent  : t -> e)
124 |     -> (attrs    : List (Attribute Select))
125 |     -> HTMLNode
126 |   selectEntries' = selectEntries @{cmap value snk}
127 |
128 |   ||| Simplified version of `selectFromListBy` that does not take
129 |   ||| a full `SelectEvent` sink.
130 |   export %inline
131 |   selectFromListBy' :
132 |        (values   : List t)
133 |     -> (sel      : t -> Bool)
134 |     -> (display  : t -> String)
135 |     -> (toEvent  : t -> e)
136 |     -> (attrs    : List (Attribute Select))
137 |     -> HTMLNode
138 |   selectFromListBy' = selectFromListBy @{cmap value snk}
139 |
140 |   ||| Simplified version of `selectFromList` that does not take
141 |   ||| a full `SelectEvent` sink.
142 |   export %inline
143 |   selectFromList' :
144 |        {auto eq : Eq t}
145 |     -> (values  : List t)
146 |     -> (init    : Maybe t)
147 |     -> (display : t -> String)
148 |     -> (toEvent : t -> e)
149 |     -> (attrs   : List (Attribute Select))
150 |     -> HTMLNode
151 |   selectFromList' = selectFromList @{cmap value snk}
152 |