diff src/ur/openid.urs @ 39:f6b3fbf10dac

Proper handling of known vs. to-be-chosen identifiers
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Jun 2011 07:51:55 -0400
parents 35bc4da563dd
children
line wrap: on
line diff
--- a/src/ur/openid.urs	Mon May 16 22:31:26 2011 -0400
+++ b/src/ur/openid.urs	Wed Jun 01 07:51:55 2011 -0400
@@ -72,6 +72,16 @@
        | Stateful of {AssociationType : association_type,
                       AssociationSessionType : association_session_type}
 
+(* It is possible to request authentication in two different modes: *)
+
+datatype authentication_mode =
+         ChooseIdentifier of string
+         (* The provider prompts the user to select his identity.
+          * The string argument should be a generic endpoint, e.g.,
+          * "https://www.google.com/accounts/o8/id". *)
+       | KnownIdentifier of string
+         (* Require authentication as this precise identifier. *)
+
 (* An authentication attempt terminates in one of four ways.
  * First, the user might get bored and surf away, never finishing the process.
  * If so, your application will never be told explicitly.
@@ -110,7 +120,7 @@
                         * crypto that you ask for, the library automatically
                         * switches to a mode that the server advertises as
                         * supported. *)
-                       Identifier : string,
+                       Identifier : authentication_mode,
                        (* The URL that the user claims identifies him.
                         * It may also point to a generic authentication service
                         * that will take care of deciding the proper