37 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
37 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
38 |
38 |
39 val orig_use_text = use_text; |
39 val orig_use_text = use_text; |
40 val orig_use_file = use_file; |
40 val orig_use_file = use_file; |
41 |
41 |
42 fun use_text name pr verbose txt = (secure_mltext (); orig_use_text name pr verbose txt); |
42 fun use_text name pr verbose txt = CRITICAL (fn () => |
43 fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name); |
43 (secure_mltext (); orig_use_text name pr verbose txt)); |
44 val use = use_file Output.ml_output true; |
44 |
|
45 fun use_file pr verbose name = CRITICAL (fn () => |
|
46 (secure_mltext (); orig_use_file pr verbose name)); |
|
47 |
|
48 fun use name = CRITICAL (fn () => use_file Output.ml_output true name); |
45 |
49 |
46 (*commit is dynamically bound!*) |
50 (*commit is dynamically bound!*) |
47 fun commit () = orig_use_text "" Output.ml_output false "commit();"; |
51 fun commit () = CRITICAL (fn () => orig_use_text "" Output.ml_output false "commit();"); |
48 |
52 |
49 |
53 |
50 (* shell commands *) |
54 (* shell commands *) |
51 |
55 |
52 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode"; |
56 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode"; |
53 |
57 |
54 val orig_execute = execute; |
58 val orig_execute = execute; |
55 val orig_system = system; |
59 val orig_system = system; |
56 |
60 |
57 fun execute s = (secure_shell (); orig_execute s); |
61 fun execute s = CRITICAL (fn () => (secure_shell (); orig_execute s)); |
58 fun system s = (secure_shell (); orig_system s); |
62 fun system s = CRITICAL (fn () => (secure_shell (); orig_system s)); |
59 |
63 |
60 end; |
64 end; |
61 |
65 |
62 val use_text = Secure.use_text; |
66 val use_text = Secure.use_text; |
63 val use_file = Secure.use_file; |
67 val use_file = Secure.use_file; |