Mercurial > gui
changeset 20:554e342665fe
Add a new parameter to Gui.gui
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 24 Sep 2011 15:47:00 -0400 |
| parents | 3a303df9ae92 |
| children | 30f9a763f5fb |
| files | calendar.ur calendar.urs datebox.ur datebox.urs examples/datebox.ur examples/togglepanel.ur gui.ur gui.urs togglePanel.ur togglePanel.urs |
| diffstat | 10 files changed, 95 insertions(+), 105 deletions(-) [+] |
line wrap: on
line diff
--- 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>)
--- 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
--- 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>)
--- 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. *)
--- 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>
--- 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>
--- 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
--- 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) [] []
--- 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)
--- 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]. *)