|
adam@18
|
1 (* This module provides generic user authentication functionality, backed by
|
|
adam@18
|
2 * OpenID authentication. Each account (named with a short alphanumeric string)
|
|
adam@18
|
3 * is associated with one or more OpenID identifiers, any of which may be used
|
|
adam@18
|
4 * to log in as that user. This module provides all the code you need to sign
|
|
adam@18
|
5 * users up, log them in, and check which user is logged in.
|
|
adam@18
|
6 *
|
|
adam@18
|
7 * Module author: Adam Chlipala
|
|
adam@18
|
8 *)
|
|
adam@18
|
9
|
|
adam@28
|
10 datatype choose_result a = Success of a | Failure of string
|
|
adam@28
|
11
|
|
kkallio@35
|
12 (* Formatting options for the gui elements and controls. *)
|
|
kkallio@35
|
13 signature CTLDISPLAY = sig
|
|
kkallio@35
|
14
|
|
kkallio@35
|
15 val formatUser : xbody -> xbody
|
|
kkallio@35
|
16 (* Format the display of the logged on user *)
|
|
kkallio@35
|
17
|
|
greenrd@48
|
18 val formatLogout : ($([]) -> transaction page) -> xbody
|
|
greenrd@48
|
19 (* Format the logout button *)
|
|
kkallio@35
|
20
|
|
kkallio@35
|
21 val formatSignup : url -> xbody
|
|
kkallio@35
|
22 (* Format the signup link *)
|
|
kkallio@35
|
23
|
|
kkallio@35
|
24 val formatLogon : ({User : string} -> transaction page) -> xbody
|
|
adam@37
|
25 (* Format the login form *)
|
|
kkallio@35
|
26 end
|
|
kkallio@35
|
27
|
|
kkallio@35
|
28 (* Some reasonable default gui control formats for programmers in a hurry. *)
|
|
kkallio@35
|
29 structure DefaultDisplay : CTLDISPLAY
|
|
kkallio@35
|
30
|
|
kkallio@35
|
31
|
|
adam@18
|
32 (* Instantiate this functor to create your customized authentication scheme. *)
|
|
adam@16
|
33 functor Make(M: sig
|
|
adam@16
|
34 con cols :: {Type}
|
|
adam@16
|
35 constraint [Id] ~ cols
|
|
adam@17
|
36 val folder : folder cols
|
|
adam@17
|
37 val inj : $(map sql_injectable cols)
|
|
adam@18
|
38 (* Extra columns of profile information to include in the user
|
|
adam@18
|
39 * database table *)
|
|
adam@16
|
40
|
|
adam@17
|
41 type creationState
|
|
adam@18
|
42 (* The type of client-side state used while soliciting sign-up
|
|
adam@18
|
43 * input *)
|
|
adam@17
|
44 type creationData
|
|
adam@18
|
45 (* A functional representation of the latest client-side state *)
|
|
adam@18
|
46
|
|
adam@17
|
47 val creationState : transaction creationState
|
|
adam@18
|
48 (* Create some fresh client-side state. *)
|
|
adam@18
|
49
|
|
adam@17
|
50 val render : creationState -> xtable
|
|
adam@18
|
51 (* Display widgets. *)
|
|
adam@18
|
52
|
|
adam@20
|
53 val ready : creationState -> signal bool
|
|
adam@20
|
54 (* Is the data ready to send? *)
|
|
adam@20
|
55
|
|
adam@17
|
56 val tabulate : creationState -> signal creationData
|
|
adam@18
|
57 (* Functionalize current state. *)
|
|
adam@18
|
58
|
|
adam@18
|
59 val choose : sql_table ([Id = string] ++ cols) [Pkey = [Id]]
|
|
adam@28
|
60 -> creationData -> transaction (choose_result $cols)
|
|
adam@18
|
61 (* Use functionalized state to choose initial column values,
|
|
adam@18
|
62 * given a handle to the users table. *)
|
|
adam@17
|
63
|
|
adam@16
|
64 val sessionLifetime : int
|
|
adam@16
|
65 (* Number of seconds a session may live *)
|
|
adam@16
|
66
|
|
adam@16
|
67 val afterLogout : url
|
|
adam@16
|
68 (* Where to send the user after he logs out *)
|
|
adam@16
|
69
|
|
adam@16
|
70 val secureCookies : bool
|
|
adam@18
|
71 (* Should authentication cookies be restricted to SSL
|
|
adam@18
|
72 * connections? *)
|
|
adam@16
|
73
|
|
adam@16
|
74 val association : Openid.association_mode
|
|
adam@16
|
75 (* OpenID cryptography preferences *)
|
|
adam@16
|
76
|
|
adam@16
|
77 val realm : option string
|
|
adam@18
|
78 (* See end of [Openid] module's documentation for the meaning
|
|
adam@18
|
79 * of realms. *)
|
|
adam@17
|
80
|
|
adam@17
|
81 val formClass : css_class
|
|
adam@18
|
82 (* CSS class for <table>, <th>, and <td> elements used in
|
|
adam@18
|
83 * sign-up form *)
|
|
adam@23
|
84
|
|
adam@23
|
85 val fakeId : option string
|
|
adam@23
|
86 (* If set, this string is always accepted as a verified
|
|
adam@23
|
87 * identifier, which can be useful during development (say,
|
|
adam@23
|
88 * when you're off-network). *)
|
|
kkallio@35
|
89
|
|
kkallio@35
|
90 structure CtlDisplay : CTLDISPLAY
|
|
kkallio@35
|
91 (* Tells how to format the GUI elements. *)
|
|
adam@16
|
92 end) : sig
|
|
adam@16
|
93
|
|
adam@16
|
94 type user
|
|
adam@28
|
95 val eq_user : eq user
|
|
adam@16
|
96 val show_user : show user
|
|
adam@28
|
97 val read_user : read user
|
|
adam@16
|
98 val inj_user : sql_injectable_prim user
|
|
adam@18
|
99 (* The abstract type of user IDs. It's really [string], but this is only
|
|
adam@18
|
100 * exposed via some standard type class instances. *)
|
|
adam@16
|
101
|
|
adam@16
|
102 table user : ([Id = user] ++ M.cols)
|
|
adam@16
|
103 PRIMARY KEY Id
|
|
adam@16
|
104
|
|
adam@16
|
105 val current : transaction (option user)
|
|
adam@18
|
106 (* Figure out which, if any, user is logged in on this connection. *)
|
|
adam@16
|
107
|
|
adam@50
|
108 val renew : transaction (option user)
|
|
adam@50
|
109 (* Like [current], but also resets the expiration time of the user's
|
|
adam@50
|
110 * session, if one is found. *)
|
|
adam@50
|
111
|
|
kkallio@35
|
112
|
|
adam@25
|
113 val main : (string -> xbody -> transaction page) -> transaction {Status : xbody,
|
|
greenrd@48
|
114 Other : {Url : option url, Xml : xbody}}
|
|
kkallio@35
|
115
|
|
adam@18
|
116 (* Pass in your generic page template; get out the HTML snippet for user
|
|
adam@18
|
117 * management, suitable for, e.g., inclusion in your standard page
|
|
adam@25
|
118 * header. The output gives a "status" chunk, which will either be a login
|
|
adam@25
|
119 * form or a message about which user is logged in; and an "other" chunk,
|
|
greenrd@48
|
120 * which will be a log out button or sign up link. In the case of "other",
|
|
greenrd@48
|
121 * the link itself (if available) is also provided for cases when one
|
|
greenrd@48
|
122 * format is not enough. *)
|
|
kkallio@35
|
123
|
|
adam@16
|
124 end
|
|
adam@26
|
125
|
|
adam@26
|
126 (* Functor outputs will contain buttons specialized to particular well-known
|
|
adam@26
|
127 * OpenID providers. Use these CSS classes to style those buttons. *)
|
|
adam@26
|
128 style aol
|
|
adam@26
|
129 style google
|
|
adam@26
|
130 style myspace
|
|
adam@26
|
131 style yahoo
|
|
adam@26
|
132
|
|
adam@26
|
133 (* This style is used by forms containing the above buttons. *)
|
|
adam@26
|
134 style provider
|
