(* TogglePanel provides a panel or section of xml which appears and
 * disappears when the user activates an associated control.  The
 * panel may contain another gui widget as content. *)

con togglePanel :: Type -> {Unit} -> Type
(* The type of appearing and disappearing panels.  The arguments
 * are as for [Gui.gui]. *)

con formatCtl = fn ctx :: {Unit} => [[Dyn] ~ ctx] =>
                   {FormatPanel : xml ([Dyn] ++ ctx) [] []
                                  -> xml ([Dyn] ++ ctx) [] []
                                  -> xml ([Dyn] ++ ctx) [] [],
                    (* Allows for formatting the panel.  The first two parameters
                     * represent "holes" for the control and panel respectively while
                     * the result should be the desired XML laying out the whole structure.
                     * The controls can be formatted with the options below.
                     * The panel part appears and disappears according to the use
                     * of the controls. *)
                  
                    OpenCtl : transaction unit -> xml ([Dyn] ++ ctx) [] [],
                    (* This should accept the transaction representing the opening of
                     * the panel and produce an XML control having this as action. *)

                    CloseCtl : transaction unit -> xml ([Dyn] ++ ctx) [] []}
                    (* This should accept the transaction representing the closing of
                     * the panel and produce an xml control having this as action. *)

(* Some reasonable default formats for the layout and controls. *)
val defaultFormat : formatCtl body'

val create : t ::: Type -> ctx ::: {Unit} ->
    formatCtl ctx    (* Formatting instructions *)
    -> t             (* Enclosed widget *)
    -> bool          (* Start in open state? *)
    -> transaction (togglePanel t ctx)

val gui_togglePanel : t ::: Type -> ctx ::: {Unit}
                      -> Gui.gui t ctx
                      -> Gui.gui (togglePanel t ctx) ctx
(* The togglePanel is itself a widget.  It can be pretty printed to a piece
 * of XML with a use of [toXml]. *)