comparison datebox.ur @ 20:554e342665fe

Add a new parameter to Gui.gui
author Adam Chlipala <adam@chlipala.net>
date Sat, 24 Sep 2011 15:47:00 -0400
parents 3a303df9ae92
children 5905b56e0cd9
comparison
equal deleted inserted replaced
19:3a303df9ae92 20:554e342665fe
1 con t other_ctx = {Cal : Calendar.t, 1 type t = {Cal : Calendar.t,
2 Panel : TogglePanel.togglePanel Calendar.t other_ctx} 2 Panel : TogglePanel.togglePanel Calendar.t []}
3 3
4 type date = Calendar.date 4 type date = Calendar.date
5 val date_eq = Calendar.date_eq 5 val date_eq = Calendar.date_eq
6 val date_ord = Calendar.date_ord 6 val date_ord = Calendar.date_ord
7 val time = Calendar.time 7 val time = Calendar.time
8 val date = Calendar.date 8 val date = Calendar.date
9 9
10 (* : other_ctx:::{Unit} -> [other_ctx ~ body] => formatCtl other_ctx *) 10 val format : TogglePanel.formatCtl [] = fn [body ~ []] =>
11 11 TogglePanel.defaultFormat
12 val format = TogglePanel.defaultFormat 12 -- #OpenCtl -- #CloseCtl
13 --#OpenCtl -- #CloseCtl 13 ++ {OpenCtl = fn behaviour => <xml><button value="Choose" onclick={behaviour}/></xml>,
14 ++ {OpenCtl = fn behaviour => <xml><button value="Choose" onclick={behaviour}/></xml>, 14 CloseCtl = fn behaviour => <xml><button value="Hide" onclick={behaviour}/></xml>}
15 CloseCtl = fn behaviour => <xml><button value="Hide" onclick={behaviour}/></xml>}
16 15
17 fun create tm = 16 fun create tm =
18 cal <- Calendar.create tm; 17 cal <- Calendar.create tm;
19 panel <- TogglePanel.create format cal False; 18 panel <- TogglePanel.create @format cal False;
20 19
21 return {Cal = cal, 20 return {Cal = cal,
22 Panel = panel} 21 Panel = panel}
23 22
24 fun onChange db f = 23 fun onChange db f =
27 fun set db day = 26 fun set db day =
28 Calendar.set db.Cal day 27 Calendar.set db.Cal day
29 28
30 fun value db = Calendar.value db.Cal 29 fun value db = Calendar.value db.Cal
31 30
32 fun render db = 31 val gui_t = Gui.mkGui (fn [body ~ []] db =>
33 <xml> 32 <xml>
34 <dyn signal={date <- Calendar.value db.Cal; 33 <dyn signal={date <- Calendar.value db.Cal;
35 return <xml>{[date.Year]}-{[date.Month]}-{[date.Day]}</xml>}/> 34 return <xml>{[date.Year]}-{[date.Month]}-{[date.Day]}</xml>}/>
36 {Gui.toXml db.Panel} 35 {Gui.toXml db.Panel}
37 </xml> 36 </xml>)