--- a/src/Pure/Concurrent/bash.ML Sat Nov 27 16:29:53 2010 +0100
+++ b/src/Pure/Concurrent/bash.ML Sat Nov 27 19:17:55 2010 +0100
@@ -4,80 +4,67 @@
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
+val bash_output = uninterruptible (fn restore_attributes => fn script =>
+ let
+ datatype result = Wait | Signal | Result of int;
+ val result = Synchronized.var "bash_result" Wait;
-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;
+ val id = serial_string ();
+ val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+ val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
+ val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
- (*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), []);
+ val system_thread =
+ Simple_Thread.fork false (fn () =>
+ Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+ let
+ val _ = File.write script_path script;
+ val status =
+ OS.Process.system
+ ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
+ File.shell_path pid_path ^ " script \"exec bash " ^
+ File.shell_path script_path ^ " > " ^
+ File.shell_path output_path ^ "\"");
+ 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 Synchronized.change result (K res) end
+ handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res)));
- (*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 ());
+ fun cleanup () =
+ (Simple_Thread.interrupt system_thread;
+ try File.rm script_path;
+ try File.rm output_path;
+ try File.rm pid_path);
+ fun kill n =
+ (case Int.fromString (File.read pid_path) 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 ());
+ in
+ let
+ (*proxy for interrupts*)
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;
+ restore_attributes (fn () =>
+ Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ()
+ handle exn => (if Exn.is_interrupt exn then kill 10 else (); reraise exn);
- (*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);
+ val output = the_default "" (try File.read output_path);
+ val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+ val _ = cleanup ();
+ in (output, rc) end
+ handle exn => (cleanup (); reraise exn)
+ end);
-end;
-
--- a/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 16:29:53 2010 +0100
+++ b/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 19:17:55 2010 +0100
@@ -5,39 +5,30 @@
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 id = serial_string ();
+ val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+ val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
+ fun cleanup () = (try File.rm script_path; try File.rm output_path);
+ in
+ let
+ val _ = File.write script_path script;
+ val status =
+ OS.Process.system
+ ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
+ " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
+ File.shell_path output_path ^ "\"");
+ 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 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 = the_default "" (try File.read output_path);
+ val _ = cleanup ();
+ in (output, rc) end
+ handle exn => (cleanup (); reraise exn)
+ end;
- 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;
-