more general bash_process, which allows to terminate background processes as well;

--- a/src/Pure/Concurrent/bash.ML	Sat Jul 16 18:11:14 2011 +0200
+++ b/src/Pure/Concurrent/bash.ML	Sat Jul 16 18:20:02 2011 +0200
@@ -4,7 +4,7 @@
 GNU bash processes, with propagation of interrupts.
 *)
 
-val bash_output = uninterruptible (fn restore_attributes => fn script =>
+val bash_process = uninterruptible (fn restore_attributes => fn script =>
   let
     datatype result = Wait | Signal | Result of int;
     val result = Synchronized.var "bash_result" Wait;
@@ -39,7 +39,9 @@
           handle exn =>
             (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
 
-    fun terminate () =
+    fun get_pid () = Int.fromString (File.read pid_path) handle IO.Io _ => NONE;
+
+    fun terminate opt_pid =
       let
         val sig_test = Posix.Signal.fromWord 0w0;
 
@@ -49,10 +51,9 @@
           handle OS.SysErr _ => false;
 
         fun kill s =
-          (case Int.fromString (File.read pid_path) of
+          (case opt_pid of
             NONE => true
-          | SOME pid => (kill_group pid s; kill_group pid sig_test))
-          handle IO.Io _ => true;
+          | SOME pid => (kill_group pid s; kill_group pid sig_test));
 
         fun multi_kill count s =
           count = 0 orelse
@@ -76,8 +77,9 @@
 
       val output = the_default "" (try File.read output_path);
       val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+      val pid = get_pid ();
       val _ = cleanup ();
-    in (output, rc) end
-    handle exn => (terminate(); cleanup (); reraise exn)
+    in {output = output, rc = rc, terminate = fn () => terminate pid} end
+    handle exn => (terminate (get_pid ()); cleanup (); reraise exn)
   end);
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash_ops.ML	Sat Jul 16 18:20:02 2011 +0200
@@ -0,0 +1,15 @@
+(*  Title:      Pure/Concurrent/bash_ops.ML
+    Author:     Makarius
+
+Derived operations for bash_process.
+*)
+
+fun bash_output s =
+  let val {output, rc, ...} = bash_process s
+  in (output, rc) end;
+
+fun bash s =
+  (case bash_output s of
+    ("", rc) => rc
+  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
+

--- a/src/Pure/Concurrent/bash_sequential.ML	Sat Jul 16 18:11:14 2011 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML	Sat Jul 16 18:20:02 2011 +0200
@@ -5,7 +5,7 @@
 could work via the controlling tty).
 *)
 
-fun bash_output script =
+fun bash_process script =
   let
     val id = serial_string ();
     val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
@@ -28,7 +28,7 @@
 
       val output = the_default "" (try File.read output_path);
       val _ = cleanup ();
-    in (output, rc) end
+    in {output = output, rc = rc, terminate = fn () => ()} end
     handle exn => (cleanup (); reraise exn)
   end;
 

--- a/src/Pure/IsaMakefile	Sat Jul 16 18:11:14 2011 +0200
+++ b/src/Pure/IsaMakefile	Sat Jul 16 18:20:02 2011 +0200
@@ -53,6 +53,7 @@
 
 $(OUT)/Pure: $(BOOTSTRAP_FILES)				\
   Concurrent/bash.ML 					\
+  Concurrent/bash_ops.ML				\
   Concurrent/bash_sequential.ML				\
   Concurrent/cache.ML					\
   Concurrent/future.ML					\

--- a/src/Pure/ROOT.ML	Sat Jul 16 18:11:14 2011 +0200
+++ b/src/Pure/ROOT.ML	Sat Jul 16 18:20:02 2011 +0200
@@ -79,11 +79,7 @@
 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/bash_ops.ML";
 
 use "Concurrent/mailbox.ML";
 use "Concurrent/task_queue.ML";