comparison togglePanel.urs @ 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 30f9a763f5fb
comparison
equal deleted inserted replaced
19:3a303df9ae92 20:554e342665fe
1 (* TogglePanel provides a panel or section of xml which appears and 1 (* TogglePanel provides a panel or section of xml which appears and
2 * disappears when the user activates an associated control. The 2 * disappears when the user activates an associated control. The
3 * panel may contain another gui widget as content. *) 3 * panel may contain another gui widget as content. *)
4 4
5 con togglePanel :: Type -> {Unit} -> Type 5 con togglePanel :: Type -> {Unit} -> Type
6 (* The type of appearing and disappearing panels. The argument 6 (* The type of appearing and disappearing panels. The arguments
7 * is the type of the content. *) 7 * are as for [Gui.gui]. *)
8 8
9 con formatCtl :: {Unit} -> Type 9 con formatCtl = fn ctx :: {Unit} => [body ~ ctx] =>
10 {FormatPanel : xbody -> xbody -> xml (body ++ ctx) [] [],
11 (* Allows for formatting the panel. The first two parameters
12 * represent "holes" for the control and panel respectively while
13 * the result should be the desired XML laying out the whole structure.
14 * The controls can be formatted with the options below.
15 * The panel part appears and disappears according to the use
16 * of the controls. *)
17
18 OpenCtl : transaction unit -> xbody,
19 (* This should accept the transaction representing the opening of
20 * the panel and produce an XML control having this as action. *)
10 21
11 (* type formatCtl = {FormatPanel : xbody -> xbody -> xbody, *) 22 CloseCtl : transaction unit -> xbody}
12 (* (\* Allows for formatting the panel. The first two parameters *) 23 (* This should accept the transaction representing the closing of
13 (* * represent "holes" for the control and panel respectively while *) 24 * the panel and produce an xml control having this as action. *)
14 (* * the result should be the desired xml laying out the whole structure. *)
15 (* * The controls can be formatted with the options below. *)
16 (* * The panel part appears and disappears according to the use *)
17 (* * of the controls. *\) *)
18
19 (* OpenCtl : transaction unit -> xbody, *)
20 (* (\* This should accept the transaction representing the opening of *)
21 (* * the panel and produce an xml control having this as action. *\) *)
22
23 (* CloseCtl : transaction unit -> xbody} *)
24 (* (\* This should accept the transaction representing the closing of *)
25 (* * the panel and produce an xml control having this as action. *\) *)
26 25
27 (* Some reasonable default formats for the layout and controls. *) 26 (* Some reasonable default formats for the layout and controls. *)
28 val defaultFormat : other_ctx:::{Unit} -> [other_ctx ~ body] => formatCtl other_ctx 27 val defaultFormat : formatCtl []
29 28
30 val create : t ::: Type -> other_ctx:::{Unit} -> [other_ctx ~ body] => 29 val create : t ::: Type -> ctx ::: {Unit} ->
31 Gui.gui t (xml ([Body] ++ other_ctx) [] []) -> formatCtl other_ctx -> t -> bool -> transaction (togglePanel t other_ctx) 30 formatCtl ctx (* Formatting instructions *)
32 (* Given instructions for formatting the display, some content and whether to start in 31 -> t (* Enclosed widget *)
33 * the open state get such a togglePanel. *) 32 -> bool (* Start in open state? *)
33 -> transaction (togglePanel t ctx)
34 34
35 val gui_togglePanel : t ::: Type -> other_ctx:::{Unit} -> [other_ctx ~ body] => 35 val gui_togglePanel : t ::: Type -> ctx ::: {Unit}
36 Gui.gui t (xml ([Body] ++ other_ctx) [] []) -> Gui.gui (togglePanel t other_ctx) (xml ([Body] ++ other_ctx) [] []) 36 -> Gui.gui t ctx
37 -> Gui.gui (togglePanel t ctx) ctx
37 (* The togglePanel is itself a widget. It can be pretty printed to a piece 38 (* The togglePanel is itself a widget. It can be pretty printed to a piece
38 * of xml with a use of toXml. *) 39 * of XML with a use of [toXml]. *)