equal
deleted
inserted
replaced
8 signature SECURE = |
8 signature SECURE = |
9 sig |
9 sig |
10 val set_secure: unit -> unit |
10 val set_secure: unit -> unit |
11 val is_secure: unit -> bool |
11 val is_secure: unit -> bool |
12 val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit |
12 val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit |
13 val evaluate: string * (unit -> 'a) option ref -> string |
|
14 -> (string -> unit) * (string -> 'b) -> bool -> string -> 'a |
|
15 val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit |
13 val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit |
16 val use_noncritical: string -> unit |
14 val use_noncritical: string -> unit |
17 val use: string -> unit |
15 val use: string -> unit |
18 val commit: unit -> unit |
16 val commit: unit -> unit |
19 val execute: string -> string |
17 val execute: string -> string |
43 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; |
44 |
42 |
45 fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () => |
43 fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () => |
46 (secure_mltext (); orig_use_text name pr verbose txt)); |
44 (secure_mltext (); orig_use_text name pr verbose txt)); |
47 |
45 |
48 (* compiler invocation as evaluation *) |
|
49 fun evaluate (ref_name, reff) name pr verbose txt = NAMED_CRITICAL name (fn () => |
|
50 let |
|
51 val _ = secure_mltext (); |
|
52 val txt' = "val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"; |
|
53 val _ = reff := NONE; |
|
54 val _ = orig_use_text name pr verbose txt'; |
|
55 in case !reff |
|
56 of NONE => error ("evaluate (" ^ ref_name ^ ")") |
|
57 | SOME f => f |
|
58 end) (); |
|
59 |
|
60 fun use_file pr verbose name = NAMED_CRITICAL "ML" (fn () => |
46 fun use_file pr verbose name = NAMED_CRITICAL "ML" (fn () => |
61 (secure_mltext (); orig_use_file pr verbose name)); |
47 (secure_mltext (); orig_use_file pr verbose name)); |
62 |
48 |
63 fun use name = use_file Output.ml_output true name; |
49 fun use name = use_file Output.ml_output true name; |
64 |
50 |
81 |
67 |
82 end; |
68 end; |
83 |
69 |
84 (*override previous toplevel bindings!*) |
70 (*override previous toplevel bindings!*) |
85 val use_text = Secure.use_text; |
71 val use_text = Secure.use_text; |
86 val evaluate = Secure.evaluate; |
|
87 val use_file = Secure.use_file; |
72 val use_file = Secure.use_file; |
88 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error"); |
73 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error"); |
89 val execute = Secure.execute; |
74 val execute = Secure.execute; |
90 val system = Secure.system; |
75 val system = Secure.system; |