changeset 19:3a303df9ae92

Partial generalize togglePanel solution (breaks build)
author Ron de Bruijn <rmbruijn@gmail.com>
date Fri, 23 Sep 2011 13:30:01 +0200
parents 16447dc6a68c
children 554e342665fe
files datebox.ur datebox.urs togglePanel.ur togglePanel.urs
diffstat 4 files changed, 41 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
--- a/datebox.ur	Thu Sep 22 19:24:01 2011 +0200
+++ b/datebox.ur	Fri Sep 23 13:30:01 2011 +0200
@@ -1,5 +1,5 @@
-type t = {Cal : Calendar.t,
-          Panel : TogglePanel.togglePanel Calendar.t}
+con t other_ctx = {Cal : Calendar.t,
+          Panel : TogglePanel.togglePanel Calendar.t other_ctx}
 
 type date = Calendar.date
 val date_eq = Calendar.date_eq
@@ -7,7 +7,9 @@
 val time = Calendar.time
 val date = Calendar.date
 
-val format = TogglePanel.defaultFormat 
+(* : other_ctx:::{Unit} -> [other_ctx ~ body] => formatCtl other_ctx  *)
+
+val format  = TogglePanel.defaultFormat 
                  --#OpenCtl -- #CloseCtl
                  ++ {OpenCtl = fn behaviour => <xml><button value="Choose" onclick={behaviour}/></xml>,
                      CloseCtl = fn behaviour => <xml><button value="Hide" onclick={behaviour}/></xml>}
--- a/datebox.urs	Thu Sep 22 19:24:01 2011 +0200
+++ b/datebox.urs	Fri Sep 23 13:30:01 2011 +0200
@@ -1,4 +1,5 @@
-type t
+con t::{Unit}->Type
+
 (* The type of dateboxes, which are input elements
  * allowing the user to select a date from a popup
  * calendar. *)
@@ -10,17 +11,17 @@
 val date : time -> date
 (* Type of dates and some useful utility functions. *)
 
-val create : time -> transaction t
+val create : other_ctx:::{Unit} -> [other_ctx ~ body] => time -> transaction (t other_ctx)
 (* Get a datebox initially set to the given time. *)
 
-val onChange : t -> (date -> transaction {}) -> transaction {}
+val onChange : other_ctx:::{Unit} -> [other_ctx ~ body] => t other_ctx -> (date -> transaction {}) -> transaction {}
 (* Add an action to be run when the date changes. *)
 
-val set : t -> date -> transaction {}
+val set : other_ctx:::{Unit} -> [other_ctx ~ body] => t other_ctx -> date -> transaction {}
 (* Call this to change the selected date. *)
 
-val value : t -> signal date
+val value : other_ctx:::{Unit} -> [other_ctx ~ body] => t other_ctx -> signal date
 (* Extract the current date value. *)
 
-val render : t -> xbody
+val render : other_ctx:::{Unit} -> [other_ctx ~ body] =>  t other_ctx -> xml ([Body] ++ other_ctx) [] []
 (* Draws the datebox as a piece of xml. *)
--- a/togglePanel.ur	Thu Sep 22 19:24:01 2011 +0200
+++ b/togglePanel.ur	Fri Sep 23 13:30:01 2011 +0200
@@ -1,27 +1,27 @@
 datatype panelState = Open | Closed
 
-type formatCtl = {FormatPanel : xbody -> xbody -> xbody,
-                  OpenCtl : transaction unit -> xbody,
-                  CloseCtl : transaction unit -> xbody}
+con formatCtl :: {Unit} -> Type = fn other_ctx => {FormatPanel : (xml ([Body] ++ other_ctx) [] []) -> (xml ([Body] ++ other_ctx) [] []) -> (xml ([Body] ++ other_ctx) [] []),
+                  OpenCtl : transaction unit -> xml ([Body] ++ other_ctx) [] [],
+                  CloseCtl : transaction unit -> xml ([Body] ++ other_ctx) [] []}
 
 val defaultFormat = {FormatPanel = fn ctl panel => <xml>{ctl}{panel}</xml>,
                      OpenCtl = fn behaviour => <xml><button value="Open" onclick={behaviour}/></xml>,
                      CloseCtl = fn behaviour => <xml><button value="Close" onclick={behaviour}/></xml>}
                     
-con togglePanel t = {PanelState : source panelState,
-                     FormatCtl : formatCtl,
+con togglePanel t other_ctx = {PanelState : source panelState,
+                     FormatCtl : formatCtl other_ctx,
                      Content : t}
 
 open Gui
 
-fun create [t ::: Type] (toXml : gui t xbody) (f : formatCtl) (content : t) (startOpen : bool) : transaction (togglePanel t) =
+fun create [t ::: Type] [other_ctx:::{Unit}] [other_ctx ~ body] (toXml : gui t (xml ([Body] ++ other_ctx) [] [])) (f : formatCtl other_ctx) (content : t) (startOpen : bool) : transaction (togglePanel t other_ctx) =
     state <- source (if startOpen then Open else Closed);
 
     return {PanelState = state,
             FormatCtl = f,
             Content = content}
 
-fun render [t ::: Type] (_ : gui t xbody) (panel : togglePanel t) =
+fun render [t ::: Type]  [other_ctx:::{Unit}] [other_ctx ~ body] (_ : gui t (xml ([Body] ++ other_ctx) [] [])) (panel : togglePanel t other_ctx) =
     let
         val openCtl = panel.FormatCtl.CloseCtl (set panel.PanelState Closed)
         val closeCtl = panel.FormatCtl.OpenCtl (set panel.PanelState Open)
@@ -48,4 +48,4 @@
             </xml>
     end
 
-fun gui_togglePanel [t ::: Type] (_ : gui t xbody) = mkGui render 
+fun gui_togglePanel [t ::: Type]  [other_ctx:::{Unit}] [other_ctx ~ body] (_ : gui t (xml ([Body] ++ other_ctx) [] [])) = mkGui render 
--- a/togglePanel.urs	Thu Sep 22 19:24:01 2011 +0200
+++ b/togglePanel.urs	Fri Sep 23 13:30:01 2011 +0200
@@ -2,33 +2,37 @@
  * disappears when the user activates an associated control.  The
  * panel may contain another gui widget as content. *)
 
-con togglePanel :: Type -> Type
+con togglePanel :: Type -> {Unit} -> Type
 (* The type of appearing and disappearing panels.  The argument
  * is the type of the content. *)
 
-type formatCtl = {FormatPanel : xbody -> xbody -> xbody,
-                  (* 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. *)
+con formatCtl :: {Unit} -> Type 
+
+(* type formatCtl = {FormatPanel : xbody -> xbody -> xbody, *)
+(*                   (\* 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 -> xbody,
-                  (* This should accept the transaction representing the opening of
-                   * the panel and produce an xml control having this as action. *)
+(*                   OpenCtl : transaction unit -> xbody, *)
+(*                   (\* This should accept the transaction representing the opening of *)
+(*                    * the panel and produce an xml control having this as action. *\) *)
 
-                  CloseCtl : transaction unit -> xbody}
-                  (* This should accept the transaction representing the closing of
-                   * the panel and produce an xml control having this as action. *)
+(*                   CloseCtl : transaction unit -> xbody} *)
+(*                   (\* This should accept the transaction representing the closing of *)
+(*                    * the panel and produce an xml control having this as action. *\) *)
 
-val defaultFormat : formatCtl
 (* Some reasonable default formats for the layout and controls. *)
+val defaultFormat :  other_ctx:::{Unit} -> [other_ctx ~ body] => formatCtl other_ctx
 
-val create : t ::: Type ->  Gui.gui t xbody -> formatCtl -> t -> bool -> transaction (togglePanel t)
+val create : t ::: Type -> other_ctx:::{Unit} -> [other_ctx ~ body] => 
+    Gui.gui t (xml ([Body] ++ other_ctx) [] []) -> formatCtl other_ctx -> t -> bool -> transaction (togglePanel t other_ctx)
 (* Given instructions for formatting the display, some content and whether to start in
  * the open state get such a togglePanel. *)
 
-val gui_togglePanel : t ::: Type -> Gui.gui t xbody -> Gui.gui (togglePanel t) xbody
+val gui_togglePanel : t ::: Type ->  other_ctx:::{Unit} -> [other_ctx ~ body] => 
+    Gui.gui t (xml ([Body] ++ other_ctx) [] []) -> Gui.gui (togglePanel t other_ctx) (xml ([Body] ++ other_ctx) [] [])
 (* The togglePanel is itself a widget.  It can be pretty printed to a piece
  * of xml with a use of toXml. *)