Mercurial > urweb
comparison doc/manual.tex @ 547:8e615bb605c9
XML
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 07 Dec 2008 10:59:14 -0500 |
| parents | 7417c4b57aeb |
| children | 39282473d38f |
comparison
equal
deleted
inserted
replaced
| 546:7417c4b57aeb | 547:8e615bb605c9 |
|---|---|
| 1195 \mt{type} \; \mt{sql\_sequence} \\ | 1195 \mt{type} \; \mt{sql\_sequence} \\ |
| 1196 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int} | 1196 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int} |
| 1197 \end{array}$$ | 1197 \end{array}$$ |
| 1198 | 1198 |
| 1199 | 1199 |
| 1200 \subsection{XML} | |
| 1201 | |
| 1202 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. | |
| 1203 | |
| 1204 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. The arguments dealing with field binding are only relevant to HTML forms. | |
| 1205 $$\begin{array}{l} | |
| 1206 \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} | |
| 1207 \end{array}$$ | |
| 1208 | |
| 1209 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. | |
| 1210 $$\begin{array}{l} | |
| 1211 \mt{con} \; \mt{tag} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} | |
| 1212 \end{array}$$ | |
| 1213 | |
| 1214 Literal text may be injected into XML as ``CDATA.'' | |
| 1215 $$\begin{array}{l} | |
| 1216 \mt{val} \; \mt{cdata} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use} ::: \{\mt{Type}\} \to \mt{string} \to \mt{xml} \; \mt{ctx} \; \mt{use} \; [] | |
| 1217 \end{array}$$ | |
| 1218 | |
| 1219 There is a function for producing an XML tree with a particular tag at its root. | |
| 1220 $$\begin{array}{l} | |
| 1221 \mt{val} \; \mt{tag} : \mt{attrsGiven} ::: \{\mt{Type}\} \to \mt{attrsAbsent} ::: \{\mt{Type}\} \to \mt{ctxOuter} ::: \{\mt{Unit}\} \to \mt{ctxInner} ::: \{\mt{Unit}\} \\ | |
| 1222 \hspace{.1in} \to \mt{useOuter} ::: \{\mt{Type}\} \to \mt{useInner} ::: \{\mt{Type}\} \to \mt{bindOuter} ::: \{\mt{Type}\} \to \mt{bindInner} ::: \{\mt{Type}\} \\ | |
| 1223 \hspace{.1in} \to \lambda [\mt{attrsGiven} \sim \mt{attrsAbsent}] \; [\mt{useOuter} \sim \mt{useInner}] \; [\mt{bindOuter} \sim \mt{bindInner}] \Rightarrow \$\mt{attrsGiven} \\ | |
| 1224 \hspace{.1in} \to \mt{tag} \; (\mt{attrsGiven} \rc \mt{attrsAbsent}) \; \mt{ctxOuter} \; \mt{ctxInner} \; \mt{useOuter} \; \mt{bindOuter} \\ | |
| 1225 \hspace{.1in} \to \mt{xml} \; \mt{ctxInner} \; \mt{useInner} \; \mt{bindInner} \to \mt{xml} \; \mt{ctxOuter} \; (\mt{useOuter} \rc \mt{useInner}) \; (\mt{bindOuter} \rc \mt{bindInner}) | |
| 1226 \end{array}$$ | |
| 1227 | |
| 1228 Two XML fragments may be concatenated. | |
| 1229 $$\begin{array}{l} | |
| 1230 \mt{val} \; \mt{join} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use_1} ::: \{\mt{Type}\} \to \mt{bind_1} ::: \{\mt{Type}\} \to \mt{bind_2} ::: \{\mt{Type}\} \\ | |
| 1231 \hspace{.1in} \to \lambda [\mt{use_1} \sim \mt{bind_1}] \; [\mt{bind_1} \sim \mt{bind_2}] \\ | |
| 1232 \hspace{.1in} \Rightarrow \mt{xml} \; \mt{ctx} \; \mt{use_1} \; \mt{bind_1} \to \mt{xml} \; \mt{ctx} \; (\mt{use_1} \rc \mt{bind_1}) \; \mt{bind_2} \to \mt{xml} \; \mt{ctx} \; \mt{use_1} \; (\mt{bind_1} \rc \mt{bind_2}) | |
| 1233 \end{array}$$ | |
| 1234 | |
| 1235 Finally, any XML fragment may be updated to ``claim'' to use more form fields than it does. | |
| 1236 $$\begin{array}{l} | |
| 1237 \mt{val} \; \mt{useMore} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use_1} ::: \{\mt{Type}\} \to \mt{use_2} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \lambda [\mt{use_1} \sim \mt{use_2}] \\ | |
| 1238 \hspace{.1in} \Rightarrow \mt{xml} \; \mt{ctx} \; \mt{use_1} \; \mt{bind} \to \mt{xml} \; \mt{ctx} \; (\mt{use_1} \rc \mt{use_2}) \; \mt{bind} | |
| 1239 \end{array}$$ | |
| 1240 | |
| 1241 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. | |
| 1242 | |
| 1243 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. | |
| 1244 $$\begin{array}{l} | |
| 1245 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t} | |
| 1246 \end{array}$$ | |
| 1247 | |
| 1200 \end{document} | 1248 \end{document} |