# HG changeset patch # User Adam Chlipala # Date 1315068665 14400 # Node ID e1f5d9c4cc20c9484065ed9abd80ef16855e613d # Parent d5c961c709f97bb34285a8cc301c10034c4a2eb4 An abstract type of IDs diff -r d5c961c709f9 -r e1f5d9c4cc20 doc/manual.tex --- a/doc/manual.tex Sat Sep 03 11:48:12 2011 -0400 +++ b/doc/manual.tex Sat Sep 03 12:51:05 2011 -0400 @@ -1983,6 +1983,17 @@ \mt{val} \; \mt{onMouseup} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \end{array}$$ +\subsubsection{Node IDs} + +There is an abstract type of node IDs that may be assigned to \cd{id} attributes of most HTML tags. + +$$\begin{array}{l} + \mt{type} \; \mt{id} \\ + \mt{val} \; \mt{fresh} : \mt{transaction} \; \mt{id} +\end{array}$$ + +The \cd{fresh} function is allowed on both server and client, but there is no other way to create IDs, which includes lack of a way to force an ID to match a particular string. The only semantic importance of IDs within Ur/Web is in uses of the HTML \cd{