Mercurial > urweb
diff 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 |
line wrap: on
line diff
--- a/doc/manual.tex Sat Dec 18 14:17:45 2010 -0500 +++ b/doc/manual.tex Sat Dec 18 15:17:09 2010 -0500 @@ -2100,15 +2100,17 @@ $$\begin{array}{l} \mt{con} \; \mt{task\_kind} :: \mt{Type} \to \mt{Type} \\ \mt{val} \; \mt{initialize} : \mt{task\_kind} \; \mt{unit} \\ -\mt{val} \; \mt{clientLeaves} : \mt{task\_kind} \; \mt{client} +\mt{val} \; \mt{clientLeaves} : \mt{task\_kind} \; \mt{client} \\ +\mt{val} \; \mt{periodic} : \mt{int} \to \mt{task\_kind} \; \mt{unit} \end{array}$$ 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}$. The currently supported task kinds are: \begin{itemize} -\item $\mt{initialize}$: Code that is run in each freshly-allocated request context. +\item $\mt{initialize}$: Code that is run when the application starts up. \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. +\item $\mt{periodic} \; n$: Code that is run when the application starts up and then every $n$ seconds thereafter. \end{itemize}