--- a/src/Pure/Concurrent/bash_sequential.ML Mon Apr 16 21:53:11 2012 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML Mon Apr 16 23:07:40 2012 +0200
@@ -7,7 +7,7 @@
signature BASH =
sig
- val process: string -> {output: string, rc: int, terminate: unit -> unit}
+ val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
end;
structure Bash: BASH =
@@ -17,16 +17,18 @@
let
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);
+ 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 output_path ^ "\"");
+ " 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
@@ -34,9 +36,10 @@
| 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 out = the_default "" (try File.read out_path);
+ val err = the_default "" (try File.read err_path);
val _ = cleanup ();
- in {output = output, rc = rc, terminate = fn () => ()} end
+ in {out = out, err = err, rc = rc, terminate = fn () => ()} end
handle exn => (cleanup (); reraise exn)
end;