--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash.ML Sat Nov 27 16:29:53 2010 +0100
@@ -0,0 +1,83 @@
+(* Title: Pure/Concurrent/bash.ML
+ Author: Makarius
+
+GNU bash processes, with propagation of interrupts.
+*)
+
+local
+
+fun read_file name =
+ let val is = TextIO.openIn name
+ in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
+
+fun write_file name txt =
+ let val os = TextIO.openOut name
+ in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
+
+in
+
+fun bash_output script =
+ Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+ let
+ val script_name = OS.FileSys.tmpName ();
+ val _ = write_file script_name script;
+
+ val pid_name = OS.FileSys.tmpName ();
+ val output_name = OS.FileSys.tmpName ();
+
+ (*result state*)
+ datatype result = Wait | Signal | Result of int;
+ val result = Unsynchronized.ref Wait;
+ val lock = Mutex.mutex ();
+ val cond = ConditionVar.conditionVar ();
+ fun set_result res =
+ (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
+
+ val _ = Mutex.lock lock;
+
+ (*system thread*)
+ val system_thread = Thread.fork (fn () =>
+ let
+ val status =
+ OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
+ " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
+ val res =
+ (case Posix.Process.fromStatus status of
+ Posix.Process.W_EXITED => Result 0
+ | Posix.Process.W_EXITSTATUS 0wx82 => Signal
+ | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
+ | Posix.Process.W_SIGNALED s =>
+ if s = Posix.Signal.int then Signal
+ else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
+ | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
+ in set_result res end handle _ (*sic*) => set_result (Result 2), []);
+
+ (*main thread -- proxy for interrupts*)
+ fun kill n =
+ (case Int.fromString (read_file pid_name) of
+ SOME pid =>
+ Posix.Process.kill
+ (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
+ Posix.Signal.int)
+ | NONE => ())
+ handle OS.SysErr _ => () | IO.Io _ =>
+ (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
+
+ val _ =
+ while ! result = Wait do
+ let val res =
+ Multithreading.sync_wait (SOME orig_atts)
+ (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
+ in if Exn.is_interrupt_exn res then kill 10 else () end;
+
+ (*cleanup*)
+ val output = read_file output_name handle IO.Io _ => "";
+ val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
+ val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
+ val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
+ val _ = Thread.interrupt system_thread handle Thread _ => ();
+ val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
+ in (output, rc) end);
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 16:29:53 2010 +0100
@@ -0,0 +1,43 @@
+(* Title: Pure/Concurrent/bash_sequential.ML
+ Author: Makarius
+
+Generic GNU bash processes (no provisions to propagate interrupts, but
+could work via the controlling tty).
+*)
+
+local
+
+fun read_file name =
+ let val is = TextIO.openIn name
+ in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
+
+fun write_file name txt =
+ let val os = TextIO.openOut name
+ in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
+
+in
+
+fun bash_output script =
+ let
+ val script_name = OS.FileSys.tmpName ();
+ val _ = write_file script_name script;
+
+ val output_name = OS.FileSys.tmpName ();
+
+ val status =
+ OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
+ " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
+ val rc =
+ (case Posix.Process.fromStatus status of
+ Posix.Process.W_EXITED => 0
+ | Posix.Process.W_EXITSTATUS w => Word8.toInt w
+ | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
+ | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
+
+ val output = read_file output_name handle IO.Io _ => "";
+ val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
+ val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
+ in (output, rc) end;
+
+end;
+
--- a/src/Pure/General/secure.ML Sat Nov 27 16:27:52 2010 +0100
+++ b/src/Pure/General/secure.ML Sat Nov 27 16:29:53 2010 +0100
@@ -15,8 +15,6 @@
val toplevel_pp: string list -> string -> unit
val PG_setup: unit -> unit
val commit: unit -> unit
- val bash_output: string -> string * int
- val bash: string -> int
end;
structure Secure: SECURE =
@@ -58,20 +56,6 @@
fun PG_setup () =
use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
-
-(* shell commands *)
-
-fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
-
-val orig_bash_output = bash_output;
-
-fun bash_output s = (secure_shell (); orig_bash_output s);
-
-fun bash s =
- (case bash_output s of
- ("", rc) => rc
- | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
-
end;
(*override previous toplevel bindings!*)
@@ -80,5 +64,4 @@
fun use s = Secure.use_file ML_Parse.global_context true s
handle ERROR msg => (writeln msg; error "ML error");
val toplevel_pp = Secure.toplevel_pp;
-val bash_output = Secure.bash_output;
-val bash = Secure.bash;
+
--- a/src/Pure/IsaMakefile Sat Nov 27 16:27:52 2010 +0100
+++ b/src/Pure/IsaMakefile Sat Nov 27 16:29:53 2010 +0100
@@ -22,7 +22,6 @@
BOOTSTRAP_FILES = \
General/exn.ML \
General/timing.ML \
- ML-Systems/bash.ML \
ML-Systems/compiler_polyml-5.2.ML \
ML-Systems/compiler_polyml-5.3.ML \
ML-Systems/ml_name_space.ML \
@@ -55,6 +54,8 @@
Pure: $(OUT)/Pure
$(OUT)/Pure: $(BOOTSTRAP_FILES) \
+ Concurrent/bash.ML \
+ Concurrent/bash_sequential.ML \
Concurrent/cache.ML \
Concurrent/future.ML \
Concurrent/lazy.ML \
--- a/src/Pure/ML-Systems/bash.ML Sat Nov 27 16:27:52 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: Pure/ML-Systems/bash.ML
- Author: Makarius
-
-Generic GNU bash processes (no provisions to propagate interrupts, but
-could work via the controlling tty).
-*)
-
-local
-
-fun read_file name =
- let val is = TextIO.openIn name
- in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
- let val os = TextIO.openOut name
- in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-in
-
-fun bash_output script =
- let
- val script_name = OS.FileSys.tmpName ();
- val _ = write_file script_name script;
-
- val output_name = OS.FileSys.tmpName ();
-
- val status =
- OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
- " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
- val rc =
- (case Posix.Process.fromStatus status of
- Posix.Process.W_EXITED => 0
- | Posix.Process.W_EXITSTATUS w => Word8.toInt w
- | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
- | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
-
- val output = read_file output_name handle IO.Io _ => "";
- val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
- val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
- in (output, rc) end;
-
-end;
-
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 16:27:52 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 16:29:53 2010 +0100
@@ -8,7 +8,6 @@
sig
val interruptible: ('a -> 'b) -> 'a -> 'b
val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
- val bash_output: string -> string * int
structure TimeLimit: TIME_LIMIT
end;
@@ -42,20 +41,6 @@
fun enabled () = max_threads_value () > 1;
-(* misc utils *)
-
-fun show "" = "" | show name = " " ^ name;
-fun show' "" = "" | show' name = " [" ^ name ^ "]";
-
-fun read_file name =
- let val is = TextIO.openIn name
- in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
- let val os = TextIO.openOut name
- in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-
(* thread attributes *)
val no_interrupts =
@@ -156,71 +141,6 @@
end;
-(* GNU bash processes, with propagation of interrupts *)
-
-fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
- let
- val script_name = OS.FileSys.tmpName ();
- val _ = write_file script_name script;
-
- val pid_name = OS.FileSys.tmpName ();
- val output_name = OS.FileSys.tmpName ();
-
- (*result state*)
- datatype result = Wait | Signal | Result of int;
- val result = ref Wait;
- val lock = Mutex.mutex ();
- val cond = ConditionVar.conditionVar ();
- fun set_result res =
- (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
-
- val _ = Mutex.lock lock;
-
- (*system thread*)
- val system_thread = Thread.fork (fn () =>
- let
- val status =
- OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
- " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
- val res =
- (case Posix.Process.fromStatus status of
- Posix.Process.W_EXITED => Result 0
- | Posix.Process.W_EXITSTATUS 0wx82 => Signal
- | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
- | Posix.Process.W_SIGNALED s =>
- if s = Posix.Signal.int then Signal
- else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
- | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
- in set_result res end handle _ (*sic*) => set_result (Result 2), []);
-
- (*main thread -- proxy for interrupts*)
- fun kill n =
- (case Int.fromString (read_file pid_name) of
- SOME pid =>
- Posix.Process.kill
- (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
- Posix.Signal.int)
- | NONE => ())
- handle OS.SysErr _ => () | IO.Io _ =>
- (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
-
- val _ =
- while ! result = Wait do
- let val res =
- sync_wait (SOME orig_atts)
- (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
- in if Exn.is_interrupt_exn res then kill 10 else () end;
-
- (*cleanup*)
- val output = read_file output_name handle IO.Io _ => "";
- val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
- val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
- val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
- val _ = Thread.interrupt system_thread handle Thread _ => ();
- val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
- in (output, rc) end);
-
-
(* critical section -- may be nested within the same thread *)
local
@@ -229,6 +149,9 @@
val critical_thread = ref (NONE: Thread.thread option);
val critical_name = ref "";
+fun show "" = "" | show name = " " ^ name;
+fun show' "" = "" | show' name = " [" ^ name ^ "]";
+
in
fun self_critical () =
--- a/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 16:27:52 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 16:29:53 2010 +0100
@@ -14,7 +14,6 @@
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
use "General/timing.ML";
-use "ML-Systems/bash.ML";
use "ML-Systems/ml_pretty.ML";
use "ML-Systems/use_context.ML";
--- a/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 16:27:52 2010 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 16:29:53 2010 +0100
@@ -14,7 +14,6 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
use "General/timing.ML";
-use "ML-Systems/bash.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
structure PolyML = struct end;
@@ -170,11 +169,6 @@
val pwd = OS.FileSys.getDir;
-(* system command execution *)
-
-val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
-
-
(* getenv *)
fun getenv var =
--- a/src/Pure/ROOT.ML Sat Nov 27 16:27:52 2010 +0100
+++ b/src/Pure/ROOT.ML Sat Nov 27 16:29:53 2010 +0100
@@ -72,6 +72,15 @@
if Multithreading.available then ()
else use "Concurrent/synchronized_sequential.ML";
+if Multithreading.available
+then use "Concurrent/bash.ML"
+else use "Concurrent/bash_sequential.ML";
+
+fun bash s =
+ (case bash_output s of
+ ("", rc) => rc
+ | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
+
use "Concurrent/mailbox.ML";
use "Concurrent/task_queue.ML";
use "Concurrent/future.ML";