kkallio@8: (* TogglePanel provides a panel or section of xml which appears and
kkallio@8:  * disappears when the user activates an associated control.  The
kkallio@8:  * panel may contain another gui widget as content. *)
kkallio@8: 
rmbruijn@19: con togglePanel :: Type -> {Unit} -> Type
adam@20: (* The type of appearing and disappearing panels.  The arguments
adam@20:  * are as for [Gui.gui]. *)
kkallio@8: 
adam@20: con formatCtl = fn ctx :: {Unit} => [body ~ ctx] =>
adam@21:                    {FormatPanel : xml (body ++ ctx) [] []
adam@21:                                   -> xml (body ++ ctx) [] []
adam@21:                                   -> xml (body ++ ctx) [] [],
adam@20:                     (* Allows for formatting the panel.  The first two parameters
adam@20:                      * represent "holes" for the control and panel respectively while
adam@20:                      * the result should be the desired XML laying out the whole structure.
adam@20:                      * The controls can be formatted with the options below.
adam@20:                      * The panel part appears and disappears according to the use
adam@20:                      * of the controls. *)
adam@20:                   
adam@21:                     OpenCtl : transaction unit -> xml (body ++ ctx) [] [],
adam@20:                     (* This should accept the transaction representing the opening of
adam@20:                      * the panel and produce an XML control having this as action. *)
rmbruijn@19: 
adam@21:                     CloseCtl : transaction unit -> xml (body ++ ctx) [] []}
adam@20:                     (* This should accept the transaction representing the closing of
adam@20:                      * the panel and produce an xml control having this as action. *)
kkallio@8: 
kkallio@8: (* Some reasonable default formats for the layout and controls. *)
adam@20: val defaultFormat : formatCtl []
kkallio@8: 
adam@20: val create : t ::: Type -> ctx ::: {Unit} ->
adam@20:     formatCtl ctx (* Formatting instructions *)
adam@20:     -> t             (* Enclosed widget *)
adam@20:     -> bool          (* Start in open state? *)
adam@20:     -> transaction (togglePanel t ctx)
kkallio@8: 
adam@20: val gui_togglePanel : t ::: Type -> ctx ::: {Unit}
adam@20:                       -> Gui.gui t ctx
adam@20:                       -> Gui.gui (togglePanel t ctx) ctx
kkallio@8: (* The togglePanel is itself a widget.  It can be pretty printed to a piece
adam@20:  * of XML with a use of [toXml]. *)