Mercurial > urweb
comparison doc/manual.tex @ 701:f963356b53fd
Update the manual
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 05 Apr 2009 12:37:38 -0400 |
parents | c90906b2f431 |
children | ec0a0dd0ca12 |
comparison
equal
deleted
inserted
replaced
700:db6ab16cd8f3 | 701:f963356b53fd |
---|---|
126 A blank line always separates the named directives from a list of modules to include in the project; if there are no named directives, a blank line must begin the file. | 126 A blank line always separates the named directives from a list of modules to include in the project; if there are no named directives, a blank line must begin the file. |
127 | 127 |
128 For each entry \texttt{M} in the module list, the file \texttt{M.urs} is included in the project if it exists, and the file \texttt{M.ur} must exist and is always included. | 128 For each entry \texttt{M} in the module list, the file \texttt{M.urs} is included in the project if it exists, and the file \texttt{M.ur} must exist and is always included. |
129 | 129 |
130 A few other named directives are supported. \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application; the default is \texttt{/}. \texttt{exe FILENAME} sets the filename to which to write the output executable; the default for file \texttt{P.urp} is \texttt{P.exe}. \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself. \texttt{profile} generates an executable that may be used with gprof. | 130 A few other named directives are supported. \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application; the default is \texttt{/}. \texttt{exe FILENAME} sets the filename to which to write the output executable; the default for file \texttt{P.urp} is \texttt{P.exe}. \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself. \texttt{profile} generates an executable that may be used with gprof. |
131 | |
132 \texttt{timeout N} sets to \texttt{N} seconds the amount of time that the generated server will wait after the last contact from a client before determining that that client has exited the application. Clients that remain active will take the timeout setting into account in determining how often to ping the server, so it only makes sense to set a high timeout to cope with browser and network delays and failures. Higher timeouts can lead to more unnecessary client information taking up memory on the server. The timeout goes unused by any page that doesn't involve the \texttt{recv} function, since the server only needs to store per-client information for clients that receive asynchronous messages. | |
133 | |
131 | 134 |
132 \subsection{Building an Application} | 135 \subsection{Building an Application} |
133 | 136 |
134 To compile project \texttt{P.urp}, simply run | 137 To compile project \texttt{P.urp}, simply run |
135 \begin{verbatim} | 138 \begin{verbatim} |
1451 $$\begin{array}{l} | 1454 $$\begin{array}{l} |
1452 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t} | 1455 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t} |
1453 \end{array}$$ | 1456 \end{array}$$ |
1454 | 1457 |
1455 | 1458 |
1456 \subsection{Functional-Reactive Client-Side Programming} | 1459 \subsection{Client-Side Programming} |
1457 | 1460 |
1458 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript. Most approaches to this kind of coding involve imperative manipulation of the DOM tree representing an HTML document's structure. Ur/Web follows the \emph{functional-reactive} approach instead. Programs may allocate mutable \emph{sources} of arbitrary types, and an HTML page is effectively a pure function over the latest values of the sources. The page is not mutated directly, but rather it changes automatically as the sources are mutated. | 1461 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript. |
1462 | |
1463 \subsubsection{The Basics} | |
1464 | |
1465 Clients can open alert dialog boxes, in the usual annoying JavaScript way. | |
1466 $$\begin{array}{l} | |
1467 \mt{val} \; \mt{alert} : \mt{string} \to \mt{transaction} \; \mt{unit} | |
1468 \end{array}$$ | |
1469 | |
1470 Any transaction may be run in a new thread with the $\mt{spawn}$ function. | |
1471 $$\begin{array}{l} | |
1472 \mt{val} \; \mt{spawn} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} | |
1473 \end{array}$$ | |
1474 | |
1475 The current thread can be paused for at least a specified number of milliseconds. | |
1476 $$\begin{array}{l} | |
1477 \mt{val} \; \mt{sleep} : \mt{int} \to \mt{transaction} \; \mt{unit} | |
1478 \end{array}$$ | |
1479 | |
1480 \subsubsection{Functional-Reactive Page Generation} | |
1481 | |
1482 Most approaches to ``AJAX''-style coding involve imperative manipulation of the DOM tree representing an HTML document's structure. Ur/Web follows the \emph{functional-reactive} approach instead. Programs may allocate mutable \emph{sources} of arbitrary types, and an HTML page is effectively a pure function over the latest values of the sources. The page is not mutated directly, but rather it changes automatically as the sources are mutated. | |
1459 | 1483 |
1460 $$\begin{array}{l} | 1484 $$\begin{array}{l} |
1461 \mt{con} \; \mt{source} :: \mt{Type} \to \mt{Type} \\ | 1485 \mt{con} \; \mt{source} :: \mt{Type} \to \mt{Type} \\ |
1462 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\ | 1486 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\ |
1463 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\ | 1487 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\ |
1473 \end{array}$$ | 1497 \end{array}$$ |
1474 | 1498 |
1475 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$. | 1499 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$. |
1476 | 1500 |
1477 $$\begin{array}{l} | 1501 $$\begin{array}{l} |
1478 \mt{val} \; \mt{dyn} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\ | 1502 \mt{val} \; \mt{dyn} : \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\ |
1479 \hspace{.1in} \to \mt{tag} \; [\mt{Signal} = \mt{signal} \; (\mt{xml} \; \mt{ctx} \; \mt{use} \; \mt{bind})] \; \mt{ctx} \; [] \; \mt{use} \; \mt{bind} | 1503 \hspace{.1in} \to \mt{tag} \; [\mt{Signal} = \mt{signal} \; (\mt{xml} \; \mt{body} \; \mt{use} \; \mt{bind})] \; \mt{body} \; [] \; \mt{use} \; \mt{bind} |
1480 \end{array}$$ | 1504 \end{array}$$ |
1481 | 1505 |
1482 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. | 1506 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. |
1507 | |
1508 \subsubsection{Asynchronous Message-Passing} | |
1509 | |
1510 To support asynchronous, ``server push'' delivery of messages to clients, any client that might need to receive an asynchronous message is assigned a unique ID. These IDs may be retrieved both on the client and on the server, during execution of code related to a client. | |
1511 | |
1512 $$\begin{array}{l} | |
1513 \mt{type} \; \mt{client} \\ | |
1514 \mt{val} \; \mt{self} : \mt{transaction} \; \mt{client} | |
1515 \end{array}$$ | |
1516 | |
1517 \emph{Channels} are the means of message-passing. Each channel is created in the context of a client and belongs to that client; no other client may receive the channel's messages. Each channel type includes the type of values that may be sent over the channel. Sending and receiving are asynchronous, in the sense that a client need not be ready to receive a message right away. Rather, sent messages may queue up, waiting to be processed. | |
1518 | |
1519 $$\begin{array}{l} | |
1520 \mt{con} \; \mt{channel} :: \mt{Type} \to \mt{Type} \\ | |
1521 \mt{val} \; \mt{channel} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; (\mt{channel} \; \mt{t}) \\ | |
1522 \mt{val} \; \mt{send} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\ | |
1523 \mt{val} \; \mt{recv} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{transaction} \; \mt{t} | |
1524 \end{array}$$ | |
1525 | |
1526 The $\mt{channel}$ and $\mt{send}$ operations may only be executed on the server, and $\mt{recv}$ may only be executed on a client. Neither clients nor channels may be passed as arguments from clients to server-side functions, so persistent channels can only be maintained by storing them in the database and looking them up using the current client ID or some application-specific value as a key. | |
1527 | |
1528 Clients and channels live only as long as the web browser page views that they are associated with. When a user surfs away, his client and its channels will be garbage-collected, after that user is not heard from for the timeout period. Garbage collection deletes any database row that contains a client or channel directly. Any reference to one of these types inside an $\mt{option}$ is set to $\mt{None}$ instead. Both kinds of handling have the flavor of weak pointers, and that is a useful way to think about clients and channels in the database. | |
1529 | |
1483 | 1530 |
1484 \section{Ur/Web Syntax Extensions} | 1531 \section{Ur/Web Syntax Extensions} |
1485 | 1532 |
1486 Ur/Web features some syntactic shorthands for building values using the functions from the last section. This section sketches the grammar of those extensions. We write spans of syntax inside brackets to indicate that they are optional. | 1533 Ur/Web features some syntactic shorthands for building values using the functions from the last section. This section sketches the grammar of those extensions. We write spans of syntax inside brackets to indicate that they are optional. |
1487 | 1534 |