(* Title: Pure/Concurrent/bash.ML
Author: Makarius
GNU bash processes, with propagation of interrupts.
*)
val bash_output = uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
val result = Synchronized.var "bash_result" Wait;
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));
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)));
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 _ =
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);
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);