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 | --------------------------------------------------------------------------------
 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 |      {auto snk : Sink e}
 42 |   -> (entries  : List (SelectEntry t))
 43 |   -> (sel      : t -> Bool)
 44 |   -> (toEvent  : t -> e)
 45 |   -> (attrs    : List (Attribute Select))
 46 |   -> HTMLNode
 47 | selectEntries es sel toEv attrs =
 48 |   select
 49 |     -- Note: The `change` event handler must be the last attribute
 50 |     --       otherwise it might already fire when the node is being
 51 |     --       set up.
 52 |     (attrs ++ [onChangeMaybe (map toEv . ix es . cast)])
 53 |     (groups [<] [<] "" 0 es >>= grp)
 54 |   where
 55 |     opt : (Nat,t,String) -> HTMLNode
 56 |     opt (x,v,s) = option [value (show x), selected (sel v)] [Text s]
 57 |
 58 |     grp : (String,List (Nat,t,String)) -> HTMLNodes
 59 |     grp ("",ps) = map opt ps
 60 |     grp (s,ps)  = [optgroup [label s] $ map opt ps]
 61 |
 62 | ||| Create a `<select>` element displaying the options in the given
 63 | ||| list.
 64 | |||
 65 | ||| @values  : the list of options
 66 | ||| @sel     : true if the given item in the list should be selected
 67 | ||| @display : how to display an option at the UI
 68 | ||| @toEvent : how to convert an option to an event
 69 | ||| @attrs   : additional attributes
 70 | export
 71 | selectFromListBy :
 72 |      {auto snk : Sink e}
 73 |   -> (values   : List t)
 74 |   -> (sel      : t -> Bool)
 75 |   -> (display  : t -> String)
 76 |   -> (toEvent  : t -> e)
 77 |   -> (attrs    : List (Attribute Select))
 78 |   -> HTMLNode
 79 | selectFromListBy vs sel f = selectEntries ((\x => Entry x $ f x) <$> vs) sel
 80 |
 81 | ||| Like `selectFromListBy` but uses an optional initial value
 82 | ||| to determine the initially selected value.
 83 | |||
 84 | ||| @values  : the list of options
 85 | ||| @init    : the initially selected option (if any)
 86 | ||| @display : how to display an option at the UI
 87 | ||| @toEvent : how to convert an option to an event
 88 | ||| @attrs   : additional attributes
 89 | export
 90 | selectFromList :
 91 |      {auto snk : Sink e}
 92 |   -> {auto eq : Eq t}
 93 |   -> (values  : List t)
 94 |   -> (init    : Maybe t)
 95 |   -> (display : t -> String)
 96 |   -> (toEvent : t -> e)
 97 |   -> (attrs   : List (Attribute Select))
 98 |   -> HTMLNode
 99 | selectFromList vs i = selectFromListBy vs ((i ==) . Just)
100 |