# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1298586545 18000
# Node ID fcd3a977d77b22fff20e9726e283b41b9a59f545
# Parent  f129ddee75f30b9b29893a3b936dc395a48d1736
More type class instances for user type; allow choose to fail

diff -r f129ddee75f3 -r fcd3a977d77b src/ur/openidUser.ur
--- a/src/ur/openidUser.ur	Sun Jan 23 17:40:42 2011 -0500
+++ b/src/ur/openidUser.ur	Thu Feb 24 17:29:05 2011 -0500
@@ -5,6 +5,8 @@
 style myspace
 style yahoo
 
+datatype choose_result a = Success of a | Failure of string
+
 functor Make(M: sig
                  con cols :: {Type}
                  constraint [Id] ~ cols
@@ -17,7 +19,7 @@
                  val render : creationState -> xtable
                  val ready : creationState -> signal bool
                  val tabulate : creationState -> signal creationData
-                 val choose : sql_table ([Id = string] ++ cols) [Pkey = [Id]] -> creationData -> transaction $cols
+                 val choose : sql_table ([Id = string] ++ cols) [Pkey = [Id]] -> creationData -> transaction (choose_result $cols)
 
                  val sessionLifetime : int
                  val afterLogout : url
@@ -29,6 +31,8 @@
              end) = struct
 
     type user = string
+    val eq_user = _
+    val read_user = _
     val show_user = _
     val inj_user = _
 
@@ -112,15 +116,18 @@
                                         None => return (Some "Invalid session data")
                                       | Some None => return (Some "Session has no associated identifier")
                                       | Some (Some ident) =>
-                                        setCookie auth {Value = LoggedIn ({User = uid} ++ ses),
-                                                        Expires = None,
-                                                        Secure = M.secureCookies};
+                                        cols <- M.choose user data;
+                                        case cols of
+                                            Failure s => return (Some s)
+                                          | Success cols =>
+                                            setCookie auth {Value = LoggedIn ({User = uid} ++ ses),
+                                                            Expires = None,
+                                                            Secure = M.secureCookies};
 
-                                        cols <- M.choose user data;
-                                        dml (insert user ({Id = (SQL {[uid]})} ++ @Sql.sqexps M.folder M.inj cols));
-                                        dml (INSERT INTO identity (User, Identifier)
-                                             VALUES ({[uid]}, {[ident]}));
-                                        redirect (bless after)
+                                            dml (insert user ({Id = (SQL {[uid]})} ++ @Sql.sqexps M.folder M.inj cols));
+                                            dml (INSERT INTO identity (User, Identifier)
+                                                 VALUES ({[uid]}, {[ident]}));
+                                            redirect (bless after)
                 in
                     uid <- source "";
                     cs <- M.creationState;
diff -r f129ddee75f3 -r fcd3a977d77b src/ur/openidUser.urs
--- a/src/ur/openidUser.urs	Sun Jan 23 17:40:42 2011 -0500
+++ b/src/ur/openidUser.urs	Thu Feb 24 17:29:05 2011 -0500
@@ -7,6 +7,8 @@
  * Module author: Adam Chlipala
  *)
 
+datatype choose_result a = Success of a | Failure of string
+
 (* Instantiate this functor to create your customized authentication scheme. *)
 functor Make(M: sig
                  con cols :: {Type}
@@ -35,7 +37,7 @@
                  (* Functionalize current state. *)
 
                  val choose : sql_table ([Id = string] ++ cols) [Pkey = [Id]]
-                              -> creationData -> transaction $cols
+                              -> creationData -> transaction (choose_result $cols)
                  (* Use functionalized state to choose initial column values,
                   * given a handle to the users table. *)
 
@@ -67,7 +69,9 @@
              end) : sig
 
     type user
+    val eq_user : eq user
     val show_user : show user
+    val read_user : read user
     val inj_user : sql_injectable_prim user
     (* The abstract type of user IDs.  It's really [string], but this is only
      * exposed via some standard type class instances. *)