diff lib/ur/basis.urs @ 1065:217eb87dde31

Basis.url and redirects
author Adam Chlipala <adamc@hcoop.net>
date Thu, 10 Dec 2009 13:32:09 -0500
parents e8a35d710ab9
children 740b85ef4352
line wrap: on
line diff
--- a/lib/ur/basis.urs	Thu Dec 10 12:06:03 2009 -0500
+++ b/lib/ur/basis.urs	Thu Dec 10 13:32:09 2009 -0500
@@ -560,8 +560,11 @@
 con tr = [Body, Tr]
 
 type url
+val show_url : show url
 val bless : string -> url
 val checkUrl : string -> option url
+val url : transaction page -> url
+val redirect : t ::: Type -> url -> transaction t
 
 val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ body] => unit
           -> tag [Signal = signal (xml (body ++ ctx) use bind)] (body ++ ctx) [] use bind