comparison doc/manual.tex @ 2047:6be31671911b

'aria-*' attributes
author Adam Chlipala <adam@chlipala.net>
date Fri, 01 Aug 2014 11:43:44 -0400
parents ced78ef1c82f
children fde864eacd47
comparison
equal deleted inserted replaced
2046:ced78ef1c82f 2047:6be31671911b
2063 \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} 2063 \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}
2064 \end{array}$$ 2064 \end{array}$$
2065 2065
2066 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, without using the foreign function interface (Section \ref{ffi}). 2066 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, without using the foreign function interface (Section \ref{ffi}).
2067 2067
2068 Some tags support HTML5 \texttt{data-*} attributes, which in Ur/Web are encoded as a single attribute $\mt{Data}$ with type $\mt{data\_attrs}$ encoding one or more attributes of this kind. See \texttt{basis.urs} for details. The usual HTML5 syntax for these attributes is supported by the Ur/Web parser as syntactic sugar. 2068 Some tags support HTML5 \texttt{data-*} attributes, which in Ur/Web are encoded as a single attribute $\mt{Data}$ with type $\mt{data\_attrs}$ encoding one or more attributes of this kind. See \texttt{basis.urs} for details. The usual HTML5 syntax for these attributes is supported by the Ur/Web parser as syntactic sugar, and the same mechanism is reused to support \texttt{aria-*} attributes.
2069 2069
2070 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. 2070 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.
2071 $$\begin{array}{l} 2071 $$\begin{array}{l}
2072 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xbody} \to \mt{t} 2072 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xbody} \to \mt{t}
2073 \end{array}$$ 2073 \end{array}$$