equal
deleted
inserted
replaced
|
1 (* Title: Pure/General/secure.ML |
|
2 ID: $Id$ |
|
3 Author: Makarius |
|
4 |
|
5 Secure critical operations. |
|
6 *) |
|
7 |
|
8 signature SECURE = |
|
9 sig |
|
10 val set_secure: unit -> bool |
|
11 val is_secure: unit -> bool |
|
12 val deny_secure: string -> unit |
|
13 val use: string -> unit |
|
14 val use_text: (string -> unit) * (string -> 'a) -> bool -> string -> unit |
|
15 val commit: unit -> unit |
|
16 end; |
|
17 |
|
18 structure Secure: SECURE = |
|
19 struct |
|
20 |
|
21 (* secure flag *) |
|
22 |
|
23 val secure = ref false; |
|
24 |
|
25 fun set_secure () = set secure; |
|
26 fun is_secure () = ! secure; |
|
27 |
|
28 fun deny_secure msg = deny (is_secure ()) msg; |
|
29 |
|
30 |
|
31 (* critical operations *) |
|
32 |
|
33 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
|
34 |
|
35 val orig_use = use; |
|
36 val orig_use_text = use_text; |
|
37 |
|
38 fun use file = (secure_mltext (); orig_use file); |
|
39 fun use_text pr verbose txt = (secure_mltext (); orig_use_text pr verbose txt); |
|
40 |
|
41 (*commit is dynamically bound!*) |
|
42 fun commit () = orig_use_text Output.ml_output false "commit();"; |
|
43 |
|
44 end; |
|
45 |
|
46 val use = Secure.use; |
|
47 val use_text = Secure.use_text; |