src/Pure/System/isabelle_system.scala

 package isabelle
 
 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
 
 import scala.io.Source
 import scala.util.matching.Regex

           }
         Map(entries: _*) +
           ("HOME" -> java.lang.System.getenv("HOME")) +
           ("PATH" -> java.lang.System.getenv("PATH"))
       }
-  }
-
-
-  /* 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 */
 

     }
   }
 
 
 
-  /** 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
-
-      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
+      val proc = new Managed_Process(false, "bash", posix_path(script_file.getPath))
+
+      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 =>
       val file = platform_file(dir + "/" + name)