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
kkallio@8: (* The type of appearing and disappearing panels.  The argument
kkallio@8:  * is the type of the content. *)
kkallio@8: 
rmbruijn@19: con formatCtl :: {Unit} -> Type 
rmbruijn@19: 
rmbruijn@19: (* type formatCtl = {FormatPanel : xbody -> xbody -> xbody, *)
rmbruijn@19: (*                   (\* Allows for formatting the panel.  The first two parameters *)
rmbruijn@19: (*                    * represent "holes" for the control and panel respectively while *)
rmbruijn@19: (*                    * the result should be the desired xml laying out the whole structure. *)
rmbruijn@19: (*                    * The controls can be formatted with the options below. *)
rmbruijn@19: (*                    * The panel part appears and disappears according to the use  *)
rmbruijn@19: (*                    * of the controls. *\) *)
kkallio@8:                   
rmbruijn@19: (*                   OpenCtl : transaction unit -> xbody, *)
rmbruijn@19: (*                   (\* This should accept the transaction representing the opening of *)
rmbruijn@19: (*                    * the panel and produce an xml control having this as action. *\) *)
kkallio@8: 
rmbruijn@19: (*                   CloseCtl : transaction unit -> xbody} *)
rmbruijn@19: (*                   (\* This should accept the transaction representing the closing of *)
rmbruijn@19: (*                    * the panel and produce an xml control having this as action. *\) *)
kkallio@8: 
kkallio@8: (* Some reasonable default formats for the layout and controls. *)
rmbruijn@19: val defaultFormat :  other_ctx:::{Unit} -> [other_ctx ~ body] => formatCtl other_ctx
kkallio@8: 
rmbruijn@19: val create : t ::: Type -> other_ctx:::{Unit} -> [other_ctx ~ body] => 
rmbruijn@19:     Gui.gui t (xml ([Body] ++ other_ctx) [] []) -> formatCtl other_ctx -> t -> bool -> transaction (togglePanel t other_ctx)
kkallio@8: (* Given instructions for formatting the display, some content and whether to start in
kkallio@8:  * the open state get such a togglePanel. *)
kkallio@8: 
rmbruijn@19: val gui_togglePanel : t ::: Type ->  other_ctx:::{Unit} -> [other_ctx ~ body] => 
rmbruijn@19:     Gui.gui t (xml ([Body] ++ other_ctx) [] []) -> Gui.gui (togglePanel t other_ctx) (xml ([Body] ++ other_ctx) [] [])
kkallio@8: (* The togglePanel is itself a widget.  It can be pretty printed to a piece
kkallio@8:  * of xml with a use of toXml. *)