equal
deleted
inserted
replaced
38 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
38 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
39 |
39 |
40 fun orig_use_text x = use_text ML_Parse.fix_ints x; |
40 fun orig_use_text x = use_text ML_Parse.fix_ints x; |
41 fun orig_use_file x = use_file ML_Parse.fix_ints x; |
41 fun orig_use_file x = use_file ML_Parse.fix_ints x; |
42 |
42 |
43 fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () => |
43 fun use_text name pr verbose txt = |
44 (secure_mltext (); orig_use_text name pr verbose txt)); |
44 (secure_mltext (); orig_use_text name pr verbose txt); |
45 |
45 |
46 fun use_file pr verbose name = NAMED_CRITICAL "ML" (fn () => |
46 fun use_file pr verbose name = |
47 (secure_mltext (); orig_use_file pr verbose name)); |
47 (secure_mltext (); orig_use_file pr verbose name); |
48 |
48 |
49 fun use name = use_file Output.ml_output true name; |
49 fun use name = use_file Output.ml_output true name; |
50 |
50 |
51 fun use_noncritical name = |
51 fun use_noncritical name = (* FIXME obsolete *) |
52 (secure_mltext (); orig_use_file Output.ml_output true name); |
52 (secure_mltext (); orig_use_file Output.ml_output true name); |
53 |
53 |
54 (*commit is dynamically bound!*) |
54 (*commit is dynamically bound!*) |
55 fun commit () = orig_use_text "" Output.ml_output false "commit();"; |
55 fun commit () = orig_use_text "" Output.ml_output false "commit();"; |
56 |
56 |