Mercurial > urweb
comparison doc/manual.tex @ 1641:68429cfce8db
Redo HTML context classification, to keep regular <body> tags out of <table> and <tr>
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 20 Dec 2011 19:02:04 -0500 |
| parents | 3bf727a08db8 |
| children | c3627f317bfd |
comparison
equal
deleted
inserted
replaced
| 1640:dc986eb6113c | 1641:68429cfce8db |
|---|---|
| 1905 | 1905 |
| 1906 \subsection{XML} | 1906 \subsection{XML} |
| 1907 | 1907 |
| 1908 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. | 1908 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. |
| 1909 | 1909 |
| 1910 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. | 1910 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. |
| 1911 $$\begin{array}{l} | 1911 $$\begin{array}{l} |
| 1912 \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} | 1912 \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} |
| 1913 \end{array}$$ | 1913 \end{array}$$ |
| 1914 | 1914 |
| 1915 We also have a type family of XML tags, indexed respectively by the record of optional attributes accepted by the tag, the context in which the tag may be placed, the context required of children of the tag, which form fields the tag uses, and which fields the tag defines. | 1915 We also have a type family of XML tags, indexed respectively by the record of optional attributes accepted by the tag, the context in which the tag may be placed, the context required of children of the tag, which form fields the tag uses, and which fields the tag defines. |
| 1954 | 1954 |
| 1955 We will not list here the different HTML tags and related functions from the standard library. They should be easy enough to understand from the code in \texttt{basis.urs}. The set of tags in the library is not yet claimed to be complete for HTML standards. Also note that there is currently no way for the programmer to add his own tags. It \emph{is} possible to add new tags directly to \texttt{basis.urs}, but this should only be done as a prelude to suggesting a patch to the main distribution. | 1955 We will not list here the different HTML tags and related functions from the standard library. They should be easy enough to understand from the code in \texttt{basis.urs}. The set of tags in the library is not yet claimed to be complete for HTML standards. Also note that there is currently no way for the programmer to add his own tags. It \emph{is} possible to add new tags directly to \texttt{basis.urs}, but this should only be done as a prelude to suggesting a patch to the main distribution. |
| 1956 | 1956 |
| 1957 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. | 1957 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. |
| 1958 $$\begin{array}{l} | 1958 $$\begin{array}{l} |
| 1959 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t} | 1959 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xbody} \to \mt{t} |
| 1960 \end{array}$$ | 1960 \end{array}$$ |
| 1961 | 1961 |
| 1962 | 1962 |
| 1963 \subsection{Client-Side Programming} | 1963 \subsection{Client-Side Programming} |
| 1964 | 1964 |
| 2048 \end{array}$$ | 2048 \end{array}$$ |
| 2049 | 2049 |
| 2050 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$. | 2050 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$. |
| 2051 | 2051 |
| 2052 $$\begin{array}{l} | 2052 $$\begin{array}{l} |
| 2053 \mt{val} \; \mt{dyn} : \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\ | 2053 \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} \\ |
| 2054 \hspace{.1in} \to \mt{tag} \; [\mt{Signal} = \mt{signal} \; (\mt{xml} \; \mt{body} \; \mt{use} \; \mt{bind})] \; \mt{body} \; [] \; \mt{use} \; \mt{bind} | 2054 \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} |
| 2055 \end{array}$$ | 2055 \end{array}$$ |
| 2056 | 2056 |
| 2057 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. | 2057 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. |
| 2058 | 2058 |
| 2059 \subsubsection{Remote Procedure Calls} | 2059 \subsubsection{Remote Procedure Calls} |