src/Pure/System/isabelle_process.scala

         List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
       new system.Managed_Process(true, cmdline: _*)
     }
     catch { case e: IOException => rm_fifos(); throw(e) }
 
+  val process_result =
+    Simple_Thread.future("process_result") { process.join }
+
   private def terminate_process()
   {
     try { process.terminate }
     catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
   }

     val (startup_failed, startup_output) =
     {
       val expired = System.currentTimeMillis() + timeout
       val result = new StringBuilder(100)
 
-      var finished = false
-      while (!finished && System.currentTimeMillis() <= expired) {
-        while (!finished && process.stdout.ready) {
+      var finished: Option[Boolean] = None
+      while (finished.isEmpty && System.currentTimeMillis() <= expired) {
+        while (finished.isEmpty && process.stdout.ready) {
           val c = process.stdout.read
-          if (c == 2) finished = true
+          if (c == 2) finished = Some(true)
           else result += c.toChar
         }
-        Thread.sleep(10)
-      }
-      (!finished, result.toString)
+        if (process_result.is_finished) finished = Some(false)
+        else Thread.sleep(10)
+      }
+      (finished.isEmpty || !finished.get, result.toString)
     }
     system_result(startup_output)
 
     if (startup_failed) {
       put_result(Markup.EXIT, "127")
       process.stdin.close
       Thread.sleep(300)
       terminate_process()
+      process_result.join
     }
     else {
       // rendezvous
       val command_stream = system.fifo_output_stream(in_fifo)
       val message_stream = system.fifo_input_stream(out_fifo)

       standard_input = stdin_actor()
       val stdout = stdout_actor()
       command_input = input_actor(command_stream)
       val message = message_actor(message_stream)
 
-      val rc = process.join
+      val rc = process_result.join
       system_result("Isabelle process terminated")
       for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
       system_result("process_manager terminated")
       put_result(Markup.EXIT, rc.toString)
     }