equal
deleted
inserted
replaced
35 |
35 |
36 (* ML evaluation *) |
36 (* ML evaluation *) |
37 |
37 |
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 val orig_use_text = use_text; |
40 fun orig_use_text x = use_text ML_Parse.fix_ints x; |
41 val orig_use_file = use_file; |
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 = NAMED_CRITICAL "ML" (fn () => |
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 = NAMED_CRITICAL "ML" (fn () => |