equal
deleted
inserted
replaced
11 val deny_secure: string -> unit |
11 val deny_secure: string -> unit |
12 val secure_mltext: unit -> unit |
12 val secure_mltext: unit -> unit |
13 val use_text: use_context -> int * string -> bool -> string -> unit |
13 val use_text: use_context -> int * string -> bool -> string -> unit |
14 val use_file: use_context -> bool -> string -> unit |
14 val use_file: use_context -> bool -> string -> unit |
15 val toplevel_pp: string list -> string -> unit |
15 val toplevel_pp: string list -> string -> unit |
16 val commit: unit -> unit |
|
17 end; |
16 end; |
18 |
17 |
19 structure Secure: SECURE = |
18 structure Secure: SECURE = |
20 struct |
19 struct |
21 |
20 |
30 |
29 |
31 |
30 |
32 |
31 |
33 (** critical operations **) |
32 (** critical operations **) |
34 |
33 |
35 (* ML evaluation *) |
|
36 |
|
37 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
34 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
38 |
35 |
39 val raw_use_text = use_text; |
36 val raw_use_text = use_text; |
40 val raw_use_file = use_file; |
37 val raw_use_file = use_file; |
41 val raw_toplevel_pp = toplevel_pp; |
38 val raw_toplevel_pp = toplevel_pp; |
43 fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt); |
40 fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt); |
44 fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name); |
41 fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name); |
45 |
42 |
46 fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp); |
43 fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp); |
47 |
44 |
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!*) |
|
54 |
|
55 end; |
45 end; |
56 |
46 |