diff -r bb6f570512b5 -r 05c3703cc6c5 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Thu Oct 12 14:07:48 2006 +0200
+++ b/src/Pure/General/secure.ML	Thu Oct 12 14:14:11 2006 +0200
@@ -13,12 +13,14 @@
   val use: string -> unit
   val use_text: (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val commit: unit -> unit
+  val execute: string -> string
+  val system: string -> int
 end;
 
 structure Secure: SECURE =
 struct
 
-(* secure flag *)
+(** secure flag **)
 
 val secure = ref false;
 
@@ -28,7 +30,9 @@
 fun deny_secure msg = deny (is_secure ()) msg;
 
 
-(* critical operations *)
+(** critical operations **)
+
+(* ML evaluation *)
 
 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
 
@@ -41,7 +45,20 @@
 (*commit is dynamically bound!*)
 fun commit () = orig_use_text Output.ml_output false "commit();";
 
+
+(* shell commands *)
+
+fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
+
+val orig_execute = execute;
+val orig_system = system;
+
+fun execute s = (secure_shell (); orig_execute s);
+fun system s = (secure_shell (); orig_system s);
+
 end;
 
 val use = Secure.use;
 val use_text = Secure.use_text;
+val execute = Secure.execute;
+val system = Secure.system;