aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur/basis.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-05-29 14:29:26 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-05-29 14:29:26 -0400
commit5b421885fdfad728ab584ef15ec1873ec3bc2a05 (patch)
tree02dc2d6caca935269cf3c6f523ad087c80d9c778 /lib/ur/basis.urs
parentf92289880fd8457a080e150cb50f0fa2af3eff9c (diff)
getHeader and setHeader
Diffstat (limited to 'lib/ur/basis.urs')
-rw-r--r--lib/ur/basis.urs10
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 09fd1a1d..bb671388 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -163,6 +163,16 @@ val setCookie : t ::: Type -> http_cookie t -> {Value : t,
Secure : bool} -> transaction unit
val clearCookie : t ::: Type -> http_cookie t -> transaction unit
+type requestHeader
+val blessRequestHeader : string -> requestHeader
+val checkRequestHeader : string -> option requestHeader
+val getHeader : requestHeader -> transaction (option string)
+
+type responseHeader
+val blessResponseHeader : string -> responseHeader
+val checkResponseHeader : string -> option responseHeader
+val setHeader : responseHeader -> string -> transaction unit
+
(** JavaScript-y gadgets *)