src/Pure/General/secure.ML
changeset 26220 d34b68c21f9a
parent 26080 d920e4c8ba82
child 26332 aa54cd3ddc9f
--- a/src/Pure/General/secure.ML	Thu Mar 06 20:17:49 2008 +0100
+++ b/src/Pure/General/secure.ML	Thu Mar 06 20:17:50 2008 +0100
@@ -14,7 +14,7 @@
   val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use: string -> unit
   val commit: unit -> unit
-  val execute: string -> string
+  val system_out: string -> string * int
   val system: string -> int
 end;
 
@@ -57,11 +57,10 @@
 
 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
 
-val orig_execute = execute;
-val orig_system = system;
+val orig_system_out = system_out;
 
-fun execute s = (secure_shell (); orig_execute s);
-fun system s = (secure_shell (); orig_system s);
+fun system_out s = (secure_shell (); orig_system_out s);
+fun system s = #2 (system_out s);
 
 end;
 
@@ -69,5 +68,5 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
-val execute = Secure.execute;
+val system_out = Secure.system_out;
 val system = Secure.system;