Mercurial > urweb
comparison doc/manual.tex @ 1349:87156c44824f
Periodic tasks
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 18 Dec 2010 15:17:09 -0500 |
| parents | 8a169fc0838b |
| children | a6d421812b93 |
comparison
equal
deleted
inserted
replaced
| 1348:8a169fc0838b | 1349:87156c44824f |
|---|---|
| 2098 In many web applications, it's useful to run code at points other than requests from browsers. Ur/Web's \emph{task} mechanism facilitates this. A type family of \emph{task kinds} is in the standard library: | 2098 In many web applications, it's useful to run code at points other than requests from browsers. Ur/Web's \emph{task} mechanism facilitates this. A type family of \emph{task kinds} is in the standard library: |
| 2099 | 2099 |
| 2100 $$\begin{array}{l} | 2100 $$\begin{array}{l} |
| 2101 \mt{con} \; \mt{task\_kind} :: \mt{Type} \to \mt{Type} \\ | 2101 \mt{con} \; \mt{task\_kind} :: \mt{Type} \to \mt{Type} \\ |
| 2102 \mt{val} \; \mt{initialize} : \mt{task\_kind} \; \mt{unit} \\ | 2102 \mt{val} \; \mt{initialize} : \mt{task\_kind} \; \mt{unit} \\ |
| 2103 \mt{val} \; \mt{clientLeaves} : \mt{task\_kind} \; \mt{client} | 2103 \mt{val} \; \mt{clientLeaves} : \mt{task\_kind} \; \mt{client} \\ |
| 2104 \mt{val} \; \mt{periodic} : \mt{int} \to \mt{task\_kind} \; \mt{unit} | |
| 2104 \end{array}$$ | 2105 \end{array}$$ |
| 2105 | 2106 |
| 2106 A task kind names a particular extension point of generated applications, where the type parameter of a task kind describes which extra input data is available at that extension point. Add task code with the special declaration form $\mt{task} \; e_1 = e_2$, where $e_1$ is a task kind with data $\tau$, and $e_2$ is a function from $\tau$ to $\mt{transaction} \; \mt{unit}$. | 2107 A task kind names a particular extension point of generated applications, where the type parameter of a task kind describes which extra input data is available at that extension point. Add task code with the special declaration form $\mt{task} \; e_1 = e_2$, where $e_1$ is a task kind with data $\tau$, and $e_2$ is a function from $\tau$ to $\mt{transaction} \; \mt{unit}$. |
| 2107 | 2108 |
| 2108 The currently supported task kinds are: | 2109 The currently supported task kinds are: |
| 2109 \begin{itemize} | 2110 \begin{itemize} |
| 2110 \item $\mt{initialize}$: Code that is run in each freshly-allocated request context. | 2111 \item $\mt{initialize}$: Code that is run when the application starts up. |
| 2111 \item $\mt{clientLeaves}$: Code that is run for each client that the runtime system decides has surfed away. When a request that generates a new client handle is aborted, that handle will still eventually be passed to $\mt{clientLeaves}$ task code, even though the corresponding browser was never informed of the client handle's existence. In other words, in general, $\mt{clientLeaves}$ handlers will be called more times than there are actual clients. | 2112 \item $\mt{clientLeaves}$: Code that is run for each client that the runtime system decides has surfed away. When a request that generates a new client handle is aborted, that handle will still eventually be passed to $\mt{clientLeaves}$ task code, even though the corresponding browser was never informed of the client handle's existence. In other words, in general, $\mt{clientLeaves}$ handlers will be called more times than there are actual clients. |
| 2113 \item $\mt{periodic} \; n$: Code that is run when the application starts up and then every $n$ seconds thereafter. | |
| 2112 \end{itemize} | 2114 \end{itemize} |
| 2113 | 2115 |
| 2114 | 2116 |
| 2115 \section{The Foreign Function Interface} | 2117 \section{The Foreign Function Interface} |
| 2116 | 2118 |