summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-11-26 14:20:00 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-11-26 14:20:00 -0500
commit20a451e11a5c10d4751beebcf09e0c86568ac5d2 (patch)
tree428c81f5418b09ac4d8f8bbfa61e16723e519f67 /doc
parent27e785f13b18b42885b15cb38a2cd48d7e8fbdd5 (diff)
More fun with cookies
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex3
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 5a46552d..866b9585 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1288,7 +1288,8 @@ $$\begin{array}{l}
\\
\mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
\mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
- \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit}
+ \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \{\mt{Value} : \mt{t}, \mt{Expires} : \mt{option} \; \mt{time}, \mt{Secure} : \mt{bool}\} \to \mt{transaction} \; \mt{unit} \\
+ \mt{val} \; \mt{clearCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; \mt{unit}
\end{array}$$
There are also an abstract $\mt{url}$ type and functions for converting to it, based on the policy defined by \texttt{[allow|deny] url} directives in the project file.