# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1316893620 14400
# Node ID 554e342665fea2a73b66a6b5d8b46907eb78efb6
# Parent  3a303df9ae925f2fbdc40e54174600340438b893
Add a new parameter to Gui.gui

diff -r 3a303df9ae92 -r 554e342665fe calendar.ur
--- a/calendar.ur	Fri Sep 23 13:30:01 2011 +0200
+++ b/calendar.ur	Sat Sep 24 15:47:00 2011 -0400
@@ -207,7 +207,7 @@
     SourceL.onChange ctl.Day f
 
 val gui_t = Gui.mkGui 
-                (fn ctl =>
+                (fn [body ~ []] ctl =>
                     <xml>
                       <dyn signal={render' ctl}/>
                     </xml>)
diff -r 3a303df9ae92 -r 554e342665fe calendar.urs
--- a/calendar.urs	Fri Sep 23 13:30:01 2011 +0200
+++ b/calendar.urs	Sat Sep 24 15:47:00 2011 -0400
@@ -20,7 +20,7 @@
 val value : t -> signal date
 (* Read the date of the calendar. *)
 
-val gui_t : Gui.gui t xbody
+val gui_t : Gui.gui t []
 (* Witness that this is a gui widget. *)
 
 val create : time -> transaction t
diff -r 3a303df9ae92 -r 554e342665fe datebox.ur
--- a/datebox.ur	Fri Sep 23 13:30:01 2011 +0200
+++ b/datebox.ur	Sat Sep 24 15:47:00 2011 -0400
@@ -1,5 +1,5 @@
-con t other_ctx = {Cal : Calendar.t,
-          Panel : TogglePanel.togglePanel Calendar.t other_ctx}
+type t = {Cal : Calendar.t,
+          Panel : TogglePanel.togglePanel Calendar.t []}
 
 type date = Calendar.date
 val date_eq = Calendar.date_eq
@@ -7,16 +7,15 @@
 val time = Calendar.time
 val date = Calendar.date
 
-(* : 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>}
+val format : TogglePanel.formatCtl [] = fn [body ~ []] =>
+    TogglePanel.defaultFormat
+        -- #OpenCtl -- #CloseCtl
+        ++ {OpenCtl = fn behaviour => <xml><button value="Choose" onclick={behaviour}/></xml>,
+            CloseCtl = fn behaviour => <xml><button value="Hide" onclick={behaviour}/></xml>}
 
 fun create tm =
     cal <- Calendar.create tm;
-    panel <- TogglePanel.create format cal False;
+    panel <- TogglePanel.create @format cal False;
 
     return {Cal = cal,
             Panel = panel}
@@ -29,9 +28,9 @@
 
 fun value db = Calendar.value db.Cal
 
-fun render db = 
+val gui_t = Gui.mkGui (fn [body ~ []] db =>
     <xml>
       <dyn signal={date <- Calendar.value db.Cal;
                    return <xml>{[date.Year]}-{[date.Month]}-{[date.Day]}</xml>}/>
       {Gui.toXml db.Panel}
-    </xml>
+    </xml>)
diff -r 3a303df9ae92 -r 554e342665fe datebox.urs
--- a/datebox.urs	Fri Sep 23 13:30:01 2011 +0200
+++ b/datebox.urs	Sat Sep 24 15:47:00 2011 -0400
@@ -1,8 +1,7 @@
-con t::{Unit}->Type
+type t
 
-(* The type of dateboxes, which are input elements
- * allowing the user to select a date from a popup
- * calendar. *)
+(* The type of dateboxes, which are input elements allowing the user to select a
+ * date from a popup calendar. *)
 
 type date = {Year : int, Month : int, Day : int}
 val date_eq : eq date
@@ -11,17 +10,17 @@
 val date : time -> date
 (* Type of dates and some useful utility functions. *)
 
-val create : other_ctx:::{Unit} -> [other_ctx ~ body] => time -> transaction (t other_ctx)
+val create : time -> transaction t
 (* Get a datebox initially set to the given time. *)
 
-val onChange : other_ctx:::{Unit} -> [other_ctx ~ body] => t other_ctx -> (date -> transaction {}) -> transaction {}
+val onChange : t -> (date -> transaction {}) -> transaction {}
 (* Add an action to be run when the date changes. *)
 
-val set : other_ctx:::{Unit} -> [other_ctx ~ body] => t other_ctx -> date -> transaction {}
+val set : t -> date -> transaction {}
 (* Call this to change the selected date. *)
 
-val value : other_ctx:::{Unit} -> [other_ctx ~ body] => t other_ctx -> signal date
+val value : t -> signal date
 (* Extract the current date value. *)
 
-val render : other_ctx:::{Unit} -> [other_ctx ~ body] =>  t other_ctx -> xml ([Body] ++ other_ctx) [] []
+val gui_t : Gui.gui t []
 (* Draws the datebox as a piece of xml. *)
diff -r 3a303df9ae92 -r 554e342665fe examples/datebox.ur
--- a/examples/datebox.ur	Fri Sep 23 13:30:01 2011 +0200
+++ b/examples/datebox.ur	Sat Sep 24 15:47:00 2011 -0400
@@ -1,15 +1,14 @@
 fun main () =
+    tm <- now;
 
-tm <- now;
+    dayCtl <- Datebox.create tm;
 
-dayCtl <- Datebox.create tm;
+    load <- return (Datebox.onChange dayCtl (fn d => alert (show d.Day)));
 
-load <- return (Datebox.onChange dayCtl (fn d => alert (show d.Day)));
-
-return
-    <xml>
-      <head><title>Datebox Example</title></head>
-      <body onload={load}>
-        {Datebox.render dayCtl}
-      </body>
-    </xml>
+    return
+        <xml>
+          <head><title>Datebox Example</title></head>
+          <body onload={load}>
+            {Gui.toXml dayCtl}
+          </body>
+        </xml>
diff -r 3a303df9ae92 -r 554e342665fe examples/togglepanel.ur
--- a/examples/togglepanel.ur	Fri Sep 23 13:30:01 2011 +0200
+++ b/examples/togglepanel.ur	Sat Sep 24 15:47:00 2011 -0400
@@ -4,14 +4,15 @@
 val defaultContent : xbody = <xml><p>Here I am inside the panel.<br/><b>Default format</b></p></xml>
 val otherContent : xbody = <xml><p>Here I am inside the panel.<br/><b>Other format</b></p></xml>
 
-val otherFormat = {FormatPanel = fn ctl panel => <xml><span>A Custom {ctl} Format</span>{panel}</xml>,
-                   OpenCtl = fn behaviour => <xml><a href={bless "http://#"} onclick={behaviour}>View</a></xml>,
-                   CloseCtl = fn behaviour => <xml><a href={bless "http://#"} onclick={behaviour}>Hide</a></xml>}
+val otherFormat = fn [body ~ []] =>
+                     {FormatPanel = fn ctl panel => <xml><span>A Custom {ctl} Format</span>{panel}</xml>,
+                      OpenCtl = fn behaviour => <xml><a href={bless "http://#"} onclick={behaviour}>View</a></xml>,
+                      CloseCtl = fn behaviour => <xml><a href={bless "http://#"} onclick={behaviour}>Hide</a></xml>}
 
 fun main () =
 
-    defaultFormatPanel <- create defaultFormat defaultContent True;
-    otherFormatPanel <- create otherFormat otherContent False;
+    defaultFormatPanel <- create @defaultFormat defaultContent True;
+    otherFormatPanel <- create @otherFormat otherContent False;
 
     return <xml>
       <head>
diff -r 3a303df9ae92 -r 554e342665fe gui.ur
--- a/gui.ur	Fri Sep 23 13:30:01 2011 +0200
+++ b/gui.ur	Sat Sep 24 15:47:00 2011 -0400
@@ -1,16 +1,8 @@
-class gui = fn t :: Type => fn xcomponent :: Type => t -> xcomponent
+class gui = fn (t :: Type) (ctx :: {Unit}) => [body ~ ctx] => t -> xml (body ++ ctx) [] []
 
-fun gui_xbody (x:xbody) : xbody = x
-fun gui_xtable (x:xtable) : xtable = x
+fun gui_xbody [body ~ []] x = x
+fun gui_xtable [body ~ _] x = x
 
-fun mkGui [t ::: Type] [xcomponent:::Type] (toXml : t -> xcomponent) = toXml 
+fun mkGui [t ::: Type] [ctx ::: {Unit}] (toXml : [body ~ ctx] => t -> xml (body ++ ctx) [] []) = @toXml
 
-fun toXml [t:::Type] [xcomponent ::: Type] (xmlize: gui t xcomponent) = xmlize 
-
-(* class gui t = t -> xbody *)
-
-(* fun toXml [t ::: Type] (xmlize : gui t) = xmlize *)
-
-(* fun gui_xbody x = x *)
-
-(* fun mkGui [t ::: Type] (toXml : t -> xbody) = toXml *)
+fun toXml [t ::: Type] [ctx ::: {Unit}] [body ~ ctx] (toXml : gui t ctx) = toXml
diff -r 3a303df9ae92 -r 554e342665fe gui.urs
--- a/gui.urs	Fri Sep 23 13:30:01 2011 +0200
+++ b/gui.urs	Sat Sep 24 15:47:00 2011 -0400
@@ -1,21 +1,17 @@
 (* Gui framework elements common across individual components. *)
 
 (* Types of this class describe gui components. *)
-class gui :: Type -> Type -> Type
- 
-
-(* class gui = fn t xcomponent => t -> xcomponent *)
-(* class gui :: Type -> Type -> Type *)
+class gui :: Type (* The type of an object to render *)
+      -> {Unit} (* The HTML context to render it for (minus [body]) *)
+      -> Type
 
 (* How to add components to the gui class. *)
-val mkGui : t ::: Type -> xcomponent:::Type -> (t -> xcomponent) -> gui t xcomponent
+val mkGui : t ::: Type -> ctx ::: {Unit} -> ([body ~ ctx] => t -> xml (body ++ ctx) [] []) -> gui t ctx
 
-(* Xml itself can be a gui component. *)
-val gui_xbody : gui xbody xbody
+(* XML itself can be a gui component. *)
+val gui_xbody : gui xbody []
+val gui_xtable : gui xtable [Table]
 
 (* Currently the only thing a gui component can do is be
  * pretty printed to a piece of xml. *)
-val toXml : t ::: Type -> xcomponent ::: Type -> gui t xcomponent -> t -> xcomponent
-
-
-
+val toXml : t ::: Type -> ctx ::: {Unit} -> [body ~ ctx] => gui t ctx -> t -> xml (body ++ ctx) [] []
diff -r 3a303df9ae92 -r 554e342665fe togglePanel.ur
--- a/togglePanel.ur	Fri Sep 23 13:30:01 2011 +0200
+++ b/togglePanel.ur	Sat Sep 24 15:47:00 2011 -0400
@@ -1,34 +1,37 @@
 datatype panelState = Open | Closed
 
-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) [] []}
+con formatCtl = fn ctx :: {Unit} => [body ~ ctx] =>
+                   {FormatPanel : xbody -> xbody -> xml (body ++ ctx) [] [],
+                    OpenCtl : transaction unit -> xbody,
+                    CloseCtl : transaction unit -> xbody}
 
-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>}
+val defaultFormat [body ~ []] =
+    {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 other_ctx = {PanelState : source panelState,
-                     FormatCtl : formatCtl other_ctx,
-                     Content : t}
+con togglePanel t ctx = {PanelState : source panelState,
+                         FormatCtl : formatCtl ctx,
+                         Content : t}
 
 open Gui
 
-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) =
+fun create [t ::: Type] [ctx ::: {Unit}] (f : formatCtl ctx) (content : t) (startOpen : bool) : transaction (togglePanel t ctx) =
     state <- source (if startOpen then Open else Closed);
 
     return {PanelState = state,
-            FormatCtl = f,
+            FormatCtl = @f,
             Content = content}
 
-fun render [t ::: Type]  [other_ctx:::{Unit}] [other_ctx ~ body] (_ : gui t (xml ([Body] ++ other_ctx) [] [])) (panel : togglePanel t other_ctx) =
+fun render [t ::: Type] [ctx ::: {Unit}] (_ : gui t ctx) [body ~ ctx] (panel : togglePanel t ctx) =
     let
-        val openCtl = panel.FormatCtl.CloseCtl (set panel.PanelState Closed)
-        val closeCtl = panel.FormatCtl.OpenCtl (set panel.PanelState Open)
+        val format = panel.FormatCtl !
+        val openCtl = format.CloseCtl (set panel.PanelState Closed)
+        val closeCtl = format.OpenCtl (set panel.PanelState Open)
 
         val content = toXml panel.Content
     in
-        panel.FormatCtl.FormatPanel
+        format.FormatPanel
             <xml>
               <dyn signal={c <- signal panel.PanelState;
                            return
@@ -48,4 +51,4 @@
             </xml>
     end
 
-fun gui_togglePanel [t ::: Type]  [other_ctx:::{Unit}] [other_ctx ~ body] (_ : gui t (xml ([Body] ++ other_ctx) [] [])) = mkGui render 
+fun gui_togglePanel [t ::: Type] [ctx ::: {Unit}] (g : gui t ctx) = mkGui (@render g)
diff -r 3a303df9ae92 -r 554e342665fe togglePanel.urs
--- a/togglePanel.urs	Fri Sep 23 13:30:01 2011 +0200
+++ b/togglePanel.urs	Sat Sep 24 15:47:00 2011 -0400
@@ -3,36 +3,37 @@
  * panel may contain another gui widget as content. *)
 
 con togglePanel :: Type -> {Unit} -> Type
-(* The type of appearing and disappearing panels.  The argument
- * is the type of the content. *)
+(* The type of appearing and disappearing panels.  The arguments
+ * are as for [Gui.gui]. *)
 
-con formatCtl :: {Unit} -> Type 
+con formatCtl = fn ctx :: {Unit} => [body ~ ctx] =>
+                   {FormatPanel : xbody -> xbody -> xml (body ++ 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 -> xbody,
+                    (* This should accept the transaction representing the opening of
+                     * the panel and produce an XML control having this as action. *)
 
-(* 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. *\) *)
-
-(*                   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. *)
 
 (* Some reasonable default formats for the layout and controls. *)
-val defaultFormat :  other_ctx:::{Unit} -> [other_ctx ~ body] => formatCtl other_ctx
+val defaultFormat : formatCtl []
 
-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 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 ->  other_ctx:::{Unit} -> [other_ctx ~ body] => 
-    Gui.gui t (xml ([Body] ++ other_ctx) [] []) -> Gui.gui (togglePanel t other_ctx) (xml ([Body] ++ other_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. *)
+ * of XML with a use of [toXml]. *)