# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1324433185 18000
# Node ID c3627f317bfd067ca8201895e9088c52fa11b3ae
# Parent  68429cfce8db6e3b3eed525feb759f1eb3c09387
Refactor HTML contexts to prevent some illegal nestings (that can crash the JavaScript runtime system)

diff -r 68429cfce8db -r c3627f317bfd doc/manual.tex
--- a/doc/manual.tex	Tue Dec 20 19:02:04 2011 -0500
+++ b/doc/manual.tex	Tue Dec 20 21:06:25 2011 -0500
@@ -1907,7 +1907,7 @@
 
 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{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.
+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{MakeForm}, \mt{Tr}]$, to indicate nesting inside a \texttt{<tr>} tag with the ability to nest \texttt{<form>} and \texttt{<dyn>} tags (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}$$
diff -r 68429cfce8db -r c3627f317bfd lib/ur/basis.urs
--- a/lib/ur/basis.urs	Tue Dec 20 19:02:04 2011 -0500
+++ b/lib/ur/basis.urs	Tue Dec 20 21:06:25 2011 -0500
@@ -664,11 +664,18 @@
 
 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 body' = [MakeForm, Body]
+con form' = [Body, Form]
+con subform' = [Body, Subform]
+con tabl' = [MakeForm, Table]
+con tr' = [MakeForm, Tr]
+
+con body = [Dyn] ++ body'
+con form = [Dyn] ++ form'
+con subform = [Dyn] ++ subform'
+con tabl = [Dyn] ++ tabl'
+con tr = [Dyn] ++ tr'
 
 con xhtml = xml html
 con page = xhtml [] []
@@ -763,10 +770,10 @@
                     Onload = transaction unit] ++ boxAttrs)
           
 val form : ctx ::: {Unit} -> bind ::: {Type}
-           -> [[Body, Form] ~ ctx] =>
+           -> [[MakeForm, Form] ~ ctx] =>
     option css_class
-    -> xml ([Body, Form] ++ ctx) [] bind
-    -> xml ([Body] ++ ctx) [] []
+    -> xml ([Form] ++ ctx) [] bind
+    -> xml ([MakeForm] ++ ctx) [] []
        
 val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
               -> [[Form] ~ ctx] =>