Node IDs

There is an abstract type of node IDs that may be assigned to id attributes of most HTML tags.

$$\begin{array}{l} \mathsf{type} \; \mathsf{id} \\ \mathsf{v... ...mathsf{fresh} : \mathsf{transaction} \; \mathsf{id} \end{array}$$

The 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 main semantic importance of IDs within Ur/Web is in uses of the HTML <label> tag. IDs play a much more central role in mainstream JavaScript programming, but Ur/Web uses a very different model to enable changes to particular nodes of a page tree, as the next manual subsection explains. IDs may still be useful in interfacing with JavaScript code (for instance, through Ur/Web's FFI).

One further use of IDs is as handles for requesting that focus be given to specific tags.

$$\begin{array}{l} \mathsf{val} \; \mathsf{giveFocus} : \mathsf{id} \to \mathsf{transaction} \; \mathsf{unit} \end{array}$$