more robust lib/scripts/process, with explicit script/no_script mode;
added general Isabelle_System.Managed_Process, with bash_output as application;
tuned;

--- a/lib/scripts/process	Wed Sep 22 00:17:35 2010 +0200
+++ b/lib/scripts/process	Wed Sep 22 00:45:42 2010 +0200
@@ -8,12 +8,9 @@
 use warnings;
 use strict;
 
-# args
+# process group
 
-my ($group, $pid_name, $cmd_line) = @ARGV;
-
-
-# process group
+my $group = $ARGV[0]; shift(@ARGV);
 
 if ($group eq "group") {
   use POSIX "setsid";
@@ -21,7 +18,9 @@
 }
 
 
-# pid
+# report pid
+
+my $pid_name = $ARGV[0]; shift(@ARGV);
 
 if ($pid_name eq "-") {
   print "$$\n";
@@ -35,5 +34,13 @@
 
 # exec process
 
-exec $cmd_line;
+my $script = $ARGV[0]; shift(@ARGV);
 
+if ($script eq "script") {
+  my $cmd_line = $ARGV[0]; shift(@ARGV);
+  exec $cmd_line || die $!;
+}
+else {
+  (exec { $ARGV[0] } @ARGV) || die $!;
+}
+

--- a/src/Pure/ML-Systems/bash.ML	Wed Sep 22 00:17:35 2010 +0200
+++ b/src/Pure/ML-Systems/bash.ML	Wed Sep 22 00:45:42 2010 +0200
@@ -25,8 +25,8 @@
     val output_name = OS.FileSys.tmpName ();
 
     val status =
-      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" nogroup /dev/null" ^
-        " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
+      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

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Sep 22 00:17:35 2010 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Sep 22 00:45:42 2010 +0200
@@ -181,7 +181,7 @@
       let
         val status =
           OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
-            " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
+            " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
         val res =
           (case Posix.Process.fromStatus status of
             Posix.Process.W_EXITED => Result 0

--- a/src/Pure/System/isabelle_system.scala	Wed Sep 22 00:17:35 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Sep 22 00:45:42 2010 +0200
@@ -9,7 +9,7 @@
 import java.util.regex.Pattern
 import java.util.Locale
 import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
-  BufferedReader, InputStreamReader, IOException}
+  BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 import java.awt.font.TextAttribute
 
@@ -71,17 +71,6 @@
   }
 
 
-  /* external processes */
-
-  def execute(redirect: Boolean, args: String*): Process =
-  {
-    val cmdline =
-      if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
-      else args
-    Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
-  }
-
-
   /* getenv */
 
   def getenv(name: String): String =
@@ -195,65 +184,105 @@
 
 
 
-  /** system tools **/
+  /** external processes **/
+
+  /* plain execute */
+
+  def execute(redirect: Boolean, args: String*): Process =
+  {
+    val cmdline =
+      if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
+      else args
+    Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
+  }
+
+
+  /* managed process */
+
+  class Managed_Process(redirect: Boolean, args: String*)
+  {
+    private val params =
+      List(expand_path("$ISABELLE_HOME/lib/scripts/process"), "group", "-", "no_script")
+    private val proc = execute(redirect, (params ++ args):_*)
+
+
+    // channels
+
+    val stdin: BufferedWriter =
+      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
+
+    val stdout: BufferedReader =
+      new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
+
+    val stderr: BufferedReader =
+      new BufferedReader(new InputStreamReader(proc.getErrorStream, Standard_System.charset))
+
+
+    // signals
+
+    private val pid = stdout.readLine
+
+    private def kill(signal: String): Boolean =
+      execute(true, "kill", "-" + signal, "-" + pid).waitFor == 0
+
+    private def multi_kill(signal: String): Boolean =
+    {
+      var running = true
+      var count = 10
+      while (running && count > 0) {
+        if (kill(signal)) {
+          Thread.sleep(100)
+          count -= 1
+        }
+        else running = false
+      }
+      running
+    }
+
+    def interrupt() { multi_kill("INT") }
+    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
+
+
+    // JVM shutdown hook
+
+    private val shutdown_hook = new Thread { override def run = terminate() }
+
+    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
+    catch { case _: IllegalStateException => }
+
+    private def cleanup() =
+      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
+      catch { case _: IllegalStateException => }
+
+
+    /* result */
+
+    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
+  }
+
+
+  /* bash */
 
   def bash(script: String): (String, String, Int) =
   {
     Standard_System.with_tmp_file("isabelle_script") { script_file =>
       Standard_System.write_file(script_file, script)
-
-      val proc =
-        execute(false, expand_path("$ISABELLE_HOME/lib/scripts/process"), "group", "-",
-          "exec bash " + posix_path(script_file.getPath))
-
-      val stdout_reader =
-        new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
-
-      val stderr_reader =
-        new BufferedReader(new InputStreamReader(proc.getErrorStream, Standard_System.charset))
-
-      val pid = stdout_reader.readLine
+      val proc = new Managed_Process(false, "bash", posix_path(script_file.getPath))
 
-      def kill(strict: Boolean) =
-      {
-        var running = true
-        var count = 10   // FIXME property!?
-        while (running && count > 0) {
-          if (execute(true, "kill", "-INT", "-" + pid).waitFor != 0)
-            running = false
-          else {
-            Thread.sleep(100)   // FIXME property!?
-            if (!strict) count -= 1
-          }
-        }
-      }
-
-      val shutdown_hook = new Thread { override def run = kill(true) }
-      Runtime.getRuntime.addShutdownHook(shutdown_hook)  // FIXME tmp file during shutdown?!?
-
-      def cleanup() =
-        try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
-        catch { case _: IllegalStateException => }
-
-      val stdout = Simple_Thread.future { Standard_System.slurp(stdout_reader) }
-      val stderr = Simple_Thread.future { Standard_System.slurp(stderr_reader) }
-      proc.getOutputStream.close
+      proc.stdin.close
+      val stdout = Simple_Thread.future { Standard_System.slurp(proc.stdout) }
+      val stderr = Simple_Thread.future { Standard_System.slurp(proc.stderr) }
 
       val rc =
-        try {
-          try { proc.waitFor }
-          catch { case e: InterruptedException => Thread.interrupted; kill(false); 2 }
-        }
-        finally {
-          stdout.join
-          stderr.join
-          proc.destroy  // FIXME kill -TERM !?
-          cleanup()
-        }
+        try { proc.join }
+        catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
       (stdout.join, stderr.join, rc)
     }
   }
 
+
+  /* system tools */
+
   def isabelle_tool(name: String, args: String*): (String, Int) =
   {
     getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>