src/Pure/General/secure.ML
changeset 26220 d34b68c21f9a
parent 26080 d920e4c8ba82
child 26332 aa54cd3ddc9f
equal deleted inserted replaced
26219:2d026932f710 26220:d34b68c21f9a
    12   val deny_secure: string -> unit
    12   val deny_secure: string -> unit
    13   val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
    13   val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
    14   val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
    14   val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
    15   val use: string -> unit
    15   val use: string -> unit
    16   val commit: unit -> unit
    16   val commit: unit -> unit
    17   val execute: string -> string
    17   val system_out: string -> string * int
    18   val system: string -> int
    18   val system: string -> int
    19 end;
    19 end;
    20 
    20 
    21 structure Secure: SECURE =
    21 structure Secure: SECURE =
    22 struct
    22 struct
    55 
    55 
    56 (* shell commands *)
    56 (* shell commands *)
    57 
    57 
    58 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
    58 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
    59 
    59 
    60 val orig_execute = execute;
    60 val orig_system_out = system_out;
    61 val orig_system = system;
       
    62 
    61 
    63 fun execute s = (secure_shell (); orig_execute s);
    62 fun system_out s = (secure_shell (); orig_system_out s);
    64 fun system s = (secure_shell (); orig_system s);
    63 fun system s = #2 (system_out s);
    65 
    64 
    66 end;
    65 end;
    67 
    66 
    68 (*override previous toplevel bindings!*)
    67 (*override previous toplevel bindings!*)
    69 val use_text = Secure.use_text;
    68 val use_text = Secure.use_text;
    70 val use_file = Secure.use_file;
    69 val use_file = Secure.use_file;
    71 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
    70 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
    72 val execute = Secure.execute;
    71 val system_out = Secure.system_out;
    73 val system = Secure.system;
    72 val system = Secure.system;