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