blob: db6e7a8bb65508b9abe37df625523bef72650823 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(********************************** A user ***********************************)
type usernameOrAnonymous
(*** Instances **)
val eq_usernameOrAnonymous : eq usernameOrAnonymous
val show_usernameOrAnonymous : show usernameOrAnonymous
(* 'read' producing a 'usernameOrAnonymous' is guaranteed to never fail, so you
can use 'readError' with impunity. *)
val read_usernameOrAnonymous : read usernameOrAnonymous
val sql_usernameOrAnonymous : sql_injectable usernameOrAnonymous
(*** Getting the username ***)
(* Grabs username out of MIT certificate. *)
val current : transaction usernameOrAnonymous
(******************************* A named user ********************************)
type username
(*** Instances **)
val eq_username : eq username
val show_username : show username
(* 'read' producing a 'username' is guaranteed to never fail, so you can use
'readError' with impunity. *)
val read_username : read username
val sql_username : sql_injectable username
(******************************** Converting *********************************)
val name : usernameOrAnonymous -> option username
val nameError : usernameOrAnonymous -> username
val orAnonymous : username -> usernameOrAnonymous
val whenIdentified : ctx ::: {Unit} -> use ::: {Type} ->
usernameOrAnonymous -> xml ctx use [] -> xml ctx use []
val whenIdentified' : ctx ::: {Unit} -> use ::: {Type} ->
usernameOrAnonymous -> (username -> xml ctx use [])
-> xml ctx use []
(* Converts a 'usernameOrAnonymous' to an 'option' tag. If anonymous, produces
empty XML. *)
val toOptionTag : use ::: {Type} -> usernameOrAnonymous -> xml select use []
|
