1.1 --- a/src/Pure/Concurrent/simple_thread.scala	Thu Jul 19 20:39:49 2012 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.scala	Thu Jul 19 20:49:17 2012 +0200
     1.3 @@ -30,11 +30,11 @@
     1.4  
     1.5    /* future result via thread */
     1.6  
     1.7 -  def future[A](name: String = "", daemon: Boolean = false)(body: => A): Future[A] =
     1.8 +  def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
     1.9    {
    1.10      val result = Future.promise[A]
    1.11 -    fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
    1.12 -    result
    1.13 +    val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
    1.14 +    (thread, result)
    1.15    }
    1.16  
    1.17  

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

     3.1 --- a/src/Pure/System/isabelle_system.scala	Thu Jul 19 20:39:49 2012 +0200
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Jul 19 20:49:17 2012 +0200
     3.3 @@ -249,8 +249,8 @@
     3.4        val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
     3.5  
     3.6        proc.stdin.close
     3.7 -      val stdout = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
     3.8 -      val stderr = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
     3.9 +      val (_, stdout) = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
    3.10 +      val (_, stderr) = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
    3.11  
    3.12        val rc =
    3.13          try { proc.join }
    3.14 @@ -261,6 +261,17 @@
    3.15  
    3.16    def bash(script: String): (String, String, Int) = bash_env(null, null, script)
    3.17  
    3.18 +  class Bash_Job(cwd: File, env: Map[String, String], script: String)
    3.19 +  {
    3.20 +    private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }
    3.21 +
    3.22 +    def terminate: Unit = thread.interrupt
    3.23 +    def is_finished: Boolean = result.is_finished
    3.24 +    def join: (String, String, Int) = result.join
    3.25 +
    3.26 +    override def toString: String = if (is_finished) join._3.toString else "<running>"
    3.27 +  }
    3.28 +
    3.29  
    3.30    /* system tools */
    3.31