1.1 --- a/src/Pure/General/secure.ML	Sat Nov 27 16:27:52 2010 +0100
     1.2 +++ b/src/Pure/General/secure.ML	Sat Nov 27 16:29:53 2010 +0100
     1.3 @@ -15,8 +15,6 @@
     1.4    val toplevel_pp: string list -> string -> unit
     1.5    val PG_setup: unit -> unit
     1.6    val commit: unit -> unit
     1.7 -  val bash_output: string -> string * int
     1.8 -  val bash: string -> int
     1.9  end;
    1.10  
    1.11  structure Secure: SECURE =
    1.12 @@ -58,20 +56,6 @@
    1.13  fun PG_setup () =
    1.14    use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
    1.15  
    1.16 -
    1.17 -(* shell commands *)
    1.18 -
    1.19 -fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
    1.20 -
    1.21 -val orig_bash_output = bash_output;
    1.22 -
    1.23 -fun bash_output s = (secure_shell (); orig_bash_output s);
    1.24 -
    1.25 -fun bash s =
    1.26 -  (case bash_output s of
    1.27 -    ("", rc) => rc
    1.28 -  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
    1.29 -
    1.30  end;
    1.31  
    1.32  (*override previous toplevel bindings!*)
    1.33 @@ -80,5 +64,4 @@
    1.34  fun use s = Secure.use_file ML_Parse.global_context true s
    1.35    handle ERROR msg => (writeln msg; error "ML error");
    1.36  val toplevel_pp = Secure.toplevel_pp;
    1.37 -val bash_output = Secure.bash_output;
    1.38 -val bash = Secure.bash;
    1.39 +