support for detached Bash_Job with some control operations;

--- a/src/Pure/Concurrent/simple_thread.scala	Thu Jul 19 20:39:49 2012 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Thu Jul 19 20:49:17 2012 +0200
@@ -30,11 +30,11 @@
 
   /* future result via thread */
 
-  def future[A](name: String = "", daemon: Boolean = false)(body: => A): Future[A] =
+  def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
   {
     val result = Future.promise[A]
-    fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
-    result
+    val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
+    (thread, result)
   }
 
 

--- a/src/Pure/System/isabelle_process.scala	Thu Jul 19 20:39:49 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Jul 19 20:49:17 2012 +0200
@@ -141,7 +141,7 @@
     }
     catch { case e: IOException => system_channel.accepted(); throw(e) }
 
-  val process_result =
+  val (_, process_result) =
     Simple_Thread.future("process_result") { process.join }
 
   private def terminate_process()

--- a/src/Pure/System/isabelle_system.scala	Thu Jul 19 20:39:49 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Jul 19 20:49:17 2012 +0200
@@ -249,8 +249,8 @@
       val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
 
       proc.stdin.close
-      val stdout = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
-      val stderr = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
+      val (_, stdout) = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
+      val (_, stderr) = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
 
       val rc =
         try { proc.join }
@@ -261,6 +261,17 @@
 
   def bash(script: String): (String, String, Int) = bash_env(null, null, script)
 
+  class Bash_Job(cwd: File, env: Map[String, String], script: String)
+  {
+    private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }
+
+    def terminate: Unit = thread.interrupt
+    def is_finished: Boolean = result.is_finished
+    def join: (String, String, Int) = result.join
+
+    override def toString: String = if (is_finished) join._3.toString else "<running>"
+  }
+
 
   /* system tools */