author | wenzelm |
Fri, 31 Oct 2014 11:18:17 +0100 | |
changeset 58842 | 22b87ab47d3b |
parent 56434 | 7acc933bd7cc |
child 58846 | 98c03412079b |
permissions | -rw-r--r-- |
20925 | 1 |
(* Title: Pure/General/secure.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Secure critical operations. |
|
5 |
*) |
|
6 |
||
7 |
signature SECURE = |
|
8 |
sig |
|
20977 | 9 |
val set_secure: unit -> unit |
20925 | 10 |
val is_secure: unit -> bool |
26080 | 11 |
val deny_secure: string -> unit |
31330 | 12 |
val secure_mltext: unit -> unit |
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
13 |
val use_text: use_context -> int * string -> bool -> string -> unit |
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
14 |
val use_file: use_context -> bool -> string -> unit |
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
29606
diff
changeset
|
15 |
val toplevel_pp: string list -> string -> unit |
20925 | 16 |
val commit: unit -> unit |
17 |
end; |
|
18 |
||
19 |
structure Secure: SECURE = |
|
20 |
struct |
|
21 |
||
20992 | 22 |
(** secure flag **) |
20925 | 23 |
|
32738 | 24 |
val secure = Unsynchronized.ref false; |
20925 | 25 |
|
20977 | 26 |
fun set_secure () = secure := true; |
20925 | 27 |
fun is_secure () = ! secure; |
28 |
||
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22144
diff
changeset
|
29 |
fun deny_secure msg = if is_secure () then error msg else (); |
20925 | 30 |
|
31 |
||
25753 | 32 |
|
20992 | 33 |
(** critical operations **) |
34 |
||
35 |
(* ML evaluation *) |
|
20925 | 36 |
|
37 |
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
|
38 |
||
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
39 |
val raw_use_text = use_text; |
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
40 |
val raw_use_file = use_file; |
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
41 |
val raw_toplevel_pp = toplevel_pp; |
20925 | 42 |
|
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
43 |
fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt); |
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
44 |
fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name); |
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
45 |
|
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
46 |
fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp); |
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
29606
diff
changeset
|
47 |
|
32739 | 48 |
|
49 |
(* global evaluation *) |
|
50 |
||
51 |
val use_global = raw_use_text ML_Parse.global_context (0, "") false; |
|
52 |
||
53 |
fun commit () = use_global "commit();"; (*commit is dynamically bound!*) |
|
37239 | 54 |
|
20925 | 55 |
end; |
56 |