--- a/src/Pure/Concurrent/bash_sequential.ML Thu Feb 18 17:07:10 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(* Title: Pure/Concurrent/bash_sequential.ML
- Author: Makarius
-
-Generic GNU bash processes (no provisions to propagate interrupts, but
-could work via the controlling tty).
-*)
-
-signature BASH =
-sig
- val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
-end;
-
-structure Bash: BASH =
-struct
-
-fun process script =
- let
- val id = serial_string ();
- val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
- val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
- val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
- fun cleanup () = (try File.rm script_path; try File.rm out_path; try File.rm err_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 out_path ^
- " 2> " ^ File.shell_path err_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 out = the_default "" (try File.read out_path);
- val err = the_default "" (try File.read err_path);
- val _ = cleanup ();
- in {out = out, err = err, rc = rc, terminate = fn () => ()} end
- handle exn => (cleanup (); reraise exn)
- end;
-
-end;
-