Redo HTML context classification, to keep regular <body> tags out of <table> and <tr>

author: Adam Chlipala <adam@chlipala.net> 2011-12-20 19:02:04 -0500
committer: Adam Chlipala <adam@chlipala.net> 2011-12-20 19:02:04 -0500
commit: 8e27e217fa4b6fbf34f588e70036fa7a21df5183 (patch)
tree: 5358ac1a4e610aa945310524d94aa0aeaf8cc3ac
parent: f7b9d1cc2d003582e03ad151bfe54f3d5fa51eb7 (diff)
6 files changed, 37 insertions, 37 deletions
diff --git a/demo/batchFun.ur b/demo/batchFun.ur
index 2b54a426..d69d68af 100644
--- a/demo/batchFun.ur
+++ b/demo/batchFun.ur
@@ -85,7 +85,7 @@ functor Make(M : sig
             <xml><dyn signal={ls <- signal lss; return <xml><table>
               <tr>
                 <th>Id</th>
-                {@mapX [colMeta] [[Body, Tr]]
+                {@mapX [colMeta] [tr]
                   (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m =>
                       <xml><th>{[m.Nam]}</th></xml>)
                   M.fl M.cols}
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index 884ab8a1..a5af8d25 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -66,7 +66,7 @@ fun replace [t] dl ls =
             set dl (Nonempty {Head = Cons (x, hd), Tail = tlS})
         end
 
-fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos len dl = <xml>
+fun renderDyn [ctx] [ctx ~ [Dyn]] [t] (f : t -> position -> xml (ctx ++ [Dyn]) [] []) filter pos len dl = <xml>
   <dyn signal={dl' <- signal dl;
                case dl' of
                    Empty => return <xml/>
@@ -119,8 +119,8 @@ fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) []
                    end}/>
 </xml>
 
-fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] [])
-    : option int -> list (t * position) -> xml (ctx ++ body) [] [] =
+fun renderFlat [ctx] [ctx ~ [Dyn]] [t] (f : t -> position -> xml (ctx ++ [Dyn]) [] [])
+    : option int -> list (t * position) -> xml (ctx ++ [Dyn]) [] [] =
     let
         fun renderFlat' len ls =
             case len of
@@ -186,10 +186,10 @@ fun sort [t] (cmp : t -> t -> signal bool) =
         sort'
     end
 
-fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
-                                          Sort : signal (option (t -> t -> signal bool)),
-                                          StartPosition : signal (option int),
-                                          MaxLength : signal (option int)}) dl = <xml>
+fun render [ctx] [ctx ~ [Dyn]] [t] f (r : {Filter : t -> signal bool,
+                                           Sort : signal (option (t -> t -> signal bool)),
+                                           StartPosition : signal (option int),
+                                           MaxLength : signal (option int)}) dl = <xml>
     <dyn signal={len <- r.MaxLength;
                  cmp <- r.Sort;
                  pos <- r.StartPosition;
diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs
index 3509ef2d..115c72be 100644
--- a/demo/more/dlist.urs
+++ b/demo/more/dlist.urs
@@ -12,11 +12,11 @@ val size : t ::: Type -> dlist t -> signal int
 val numPassing : t ::: Type -> (t -> signal bool) -> dlist t -> signal int
 val foldl : t ::: Type -> acc ::: Type -> (t -> acc -> signal acc) -> acc -> dlist t -> signal acc
 
-val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type
-             -> (t -> position -> xml (ctx ++ body) [] [])
+val render : ctx ::: {Unit} -> [ctx ~ [Dyn]] => t ::: Type
+             -> (t -> position -> xml (ctx ++ [Dyn]) [] [])
              -> {StartPosition : signal (option int),
                  MaxLength : signal (option int),
                  Filter : t -> signal bool,
                  Sort : signal (option (t -> t -> signal bool)) (* <= *)}
              -> dlist t
-             -> xml (ctx ++ body) [] []
+             -> xml (ctx ++ [Dyn]) [] []
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
index 9375e811..dd0cb813 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -125,7 +125,7 @@ functor Make(M : sig
       <table class={tabl}>
         <tr class={tr}>
           <th/> <th/> <th><button value="No sort" onclick={set grid.Sort None}/></th>
-          {@mapX2 [fst3] [colMeta M.row] [[Body, Tr]]
+          {@mapX2 [fst3] [colMeta M.row] [tr]
             (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
                              data (meta : colMeta M.row p) =>
                 <xml><th class={th}>
diff --git a/doc/manual.tex b/doc/manual.tex
index 48adf2a2..23b7b3be 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1907,7 +1907,7 @@ $$\begin{array}{l}
 
 Ur/Web's library contains an encoding of XML syntax and semantic constraints.  We make no effort to follow the standards governing XML schemas.  Rather, XML fragments are viewed more as values of ML datatypes, and we only track which tags are allowed inside which other tags.  The Ur/Web standard library encodes a very loose version of XHTML, where it is very easy to produce documents which are invalid XHTML, but which still display properly in all major browsers.  The main purposes of the invariants that are enforced are first, to provide some documentation about the places where it would make sense to insert XML fragments; and second, to rule out code injection attacks and other abstraction violations related to HTML syntax.
 
-The basic XML type family has arguments respectively indicating the \emph{context} of a fragment, the fields that the fragment expects to be bound on entry (and their types), and the fields that the fragment will bind (and their types).  Contexts are a record-based ``poor man's subtyping'' encoding, with each possible set of valid tags corresponding to a different context record.  For instance, the context for the \texttt{<td>} tag is $[\mt{Body}, \mt{Tr}]$, to indicate a kind of nesting inside \texttt{<body>} and \texttt{<tr>}.  Contexts are maintained in a somewhat ad-hoc way; the only definitive reference for their meanings is the types of the tag values in \texttt{basis.urs}.  The arguments dealing with field binding are only relevant to HTML forms.
+The basic XML type family has arguments respectively indicating the \emph{context} of a fragment, the fields that the fragment expects to be bound on entry (and their types), and the fields that the fragment will bind (and their types).  Contexts are a record-based ``poor man's subtyping'' encoding, with each possible set of valid tags corresponding to a different context record.  For instance, the context for the \texttt{<td>} tag is $[\mt{Dyn}, \mt{Tr}]$, to indicate nesting inside a \texttt{<tr>} tag with the ability to use the \texttt{<dyn>} tag (see below).  Contexts are maintained in a somewhat ad-hoc way; the only definitive reference for their meanings is the types of the tag values in \texttt{basis.urs}.  The arguments dealing with field binding are only relevant to HTML forms.
 $$\begin{array}{l}
   \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
 \end{array}$$
@@ -1956,7 +1956,7 @@ We will not list here the different HTML tags and related functions from the sta
 
 One last useful function is for aborting any page generation, returning some XML as an error message.  This function takes the place of some uses of a general exception mechanism.
 $$\begin{array}{l}
-  \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t}
+  \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xbody} \to \mt{t}
 \end{array}$$
 
 
@@ -2050,8 +2050,8 @@ $$\begin{array}{l}
 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$.
 
 $$\begin{array}{l}
-  \mt{val} \; \mt{dyn} : \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\
-  \hspace{.1in} \to \mt{tag} \; [\mt{Signal} = \mt{signal} \; (\mt{xml} \; \mt{body} \; \mt{use} \; \mt{bind})] \; \mt{body} \; [] \; \mt{use} \; \mt{bind}
+  \mt{val} \; \mt{dyn} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to [\mt{ctx} \sim [\mt{Dyn}]] \Rightarrow \mt{unit} \\
+  \hspace{.1in} \to \mt{tag} \; [\mt{Signal} = \mt{signal} \; (\mt{xml} \; ([\mt{Dyn}] \rc \mt{ctx}) \; \mt{use} \; \mt{bind})] \; ([\mt{Dyn}] \rc \mt{ctx}) \; [] \; \mt{use} \; \mt{bind}
 \end{array}$$
 
 Transactions can be run on the client by including them in attributes like the $\mt{Onclick}$ attribute of $\mt{button}$, and GUI widgets like $\mt{ctextbox}$ have $\mt{Source}$ attributes that can be used to connect them to sources, so that their values can be read by code running because of, e.g., an $\mt{Onclick}$ event.
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 83f23cae..a2209150 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -662,24 +662,24 @@ val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
                     xml ctx use1 bind
                     -> xml ctx (use1 ++ use2) bind
 
-con xhtml = xml [Html]
+con html = [Html]
+con head = [Head]
+con body = [Dyn, Body]
+con form = [Dyn, Body, Form]
+con subform = [Dyn, Body, Subform]
+con tabl = [Dyn, Table]
+con tr = [Dyn, Tr]
+
+con xhtml = xml html
 con page = xhtml [] []
-con xbody = xml [Body] [] []
-con xtable = xml [Body, Table] [] []
-con xtr = xml [Body, Tr] [] []
-con xform = xml [Body, Form] [] []
+con xbody = xml body [] []
+con xtable = xml tabl [] []
+con xtr = xml tr [] []
+con xform = xml form [] []
 
 
 (*** HTML details *)
 
-con html = [Html]
-con head = [Head]
-con body = [Body]
-con form = [Body, Form]
-con subform = [Body, Subform]
-con tabl = [Body, Table]
-con tr = [Body, Tr]
-
 type queryString
 val show_queryString : show queryString
 
@@ -697,8 +697,8 @@ val redirect : t ::: Type -> url -> transaction t
 type id
 val fresh : transaction id
 
-val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ body] => unit
-          -> tag [Signal = signal (xml (body ++ ctx) use bind)] (body ++ ctx) [] use bind
+val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ [Dyn]] => unit
+          -> tag [Signal = signal (xml ([Dyn] ++ ctx) use bind)] ([Dyn] ++ ctx) [] use bind
 
 val head : unit -> tag [] html head [] []
 val title : unit -> tag [] head [] [] []
@@ -763,7 +763,7 @@ val img : bodyTag ([Alt = string, Src = url, Width = int, Height = int,
                     Onload = transaction unit] ++ boxAttrs)
           
 val form : ctx ::: {Unit} -> bind ::: {Type}
-           -> [[Body, Form, Table] ~ ctx] =>
+           -> [[Body, Form] ~ ctx] =>
     option css_class
     -> xml ([Body, Form] ++ ctx) [] bind
     -> xml ([Body] ++ ctx) [] []
@@ -864,16 +864,16 @@ val ctextarea : cformTag ([Value = string, Rows = int, Cols = int, Source = sour
 
 val tabl : other ::: {Unit} -> [other ~ [Body, Table]] => unit
   -> tag ([Border = int] ++ boxAttrs)
-         ([Body] ++ other) ([Body, Table] ++ other) [] []
-val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] => unit
+         ([Body] ++ other) ([Table] ++ other) [] []
+val tr : other ::: {Unit} -> [other ~ [Table, Tr]] => unit
   -> tag tableAttrs
-         ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
+         ([Table] ++ other) ([Tr] ++ other) [] []
 val th : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
   -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
-         ([Body, Tr] ++ other) ([Body] ++ other) [] []
+         ([Tr] ++ other) ([Body] ++ other) [] []
 val td : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
   -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
-         ([Body, Tr] ++ other) ([Body] ++ other) [] []
+         ([Tr] ++ other) ([Body] ++ other) [] []
 
 
 (** Aborting *)
author	Adam Chlipala <adam@chlipala.net>	2011-12-20 19:02:04 -0500
committer	Adam Chlipala <adam@chlipala.net>	2011-12-20 19:02:04 -0500
commit	8e27e217fa4b6fbf34f588e70036fa7a21df5183 (patch)
tree	5358ac1a4e610aa945310524d94aa0aeaf8cc3ac
parent	f7b9d1cc2d003582e03ad151bfe54f3d5fa51eb7 (diff)