src/Pure/System/isabelle_process.scala
changeset 39587 f84b70e3bb9c
parent 39585 00be8711082f
child 39591 a43a723753e6
     1.1 --- a/src/Pure/System/isabelle_process.scala	Wed Sep 22 14:06:48 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Sep 22 14:29:13 2010 +0200
     1.3 @@ -136,6 +136,9 @@
     1.4      }
     1.5      catch { case e: IOException => rm_fifos(); throw(e) }
     1.6  
     1.7 +  val process_result =
     1.8 +    Simple_Thread.future("process_result") { process.join }
     1.9 +
    1.10    private def terminate_process()
    1.11    {
    1.12      try { process.terminate }
    1.13 @@ -149,16 +152,17 @@
    1.14        val expired = System.currentTimeMillis() + timeout
    1.15        val result = new StringBuilder(100)
    1.16  
    1.17 -      var finished = false
    1.18 -      while (!finished && System.currentTimeMillis() <= expired) {
    1.19 -        while (!finished && process.stdout.ready) {
    1.20 +      var finished: Option[Boolean] = None
    1.21 +      while (finished.isEmpty && System.currentTimeMillis() <= expired) {
    1.22 +        while (finished.isEmpty && process.stdout.ready) {
    1.23            val c = process.stdout.read
    1.24 -          if (c == 2) finished = true
    1.25 +          if (c == 2) finished = Some(true)
    1.26            else result += c.toChar
    1.27          }
    1.28 -        Thread.sleep(10)
    1.29 +        if (process_result.is_finished) finished = Some(false)
    1.30 +        else Thread.sleep(10)
    1.31        }
    1.32 -      (!finished, result.toString)
    1.33 +      (finished.isEmpty || !finished.get, result.toString)
    1.34      }
    1.35      system_result(startup_output)
    1.36  
    1.37 @@ -167,6 +171,7 @@
    1.38        process.stdin.close
    1.39        Thread.sleep(300)
    1.40        terminate_process()
    1.41 +      process_result.join
    1.42      }
    1.43      else {
    1.44        // rendezvous
    1.45 @@ -178,7 +183,7 @@
    1.46        command_input = input_actor(command_stream)
    1.47        val message = message_actor(message_stream)
    1.48  
    1.49 -      val rc = process.join
    1.50 +      val rc = process_result.join
    1.51        system_result("Isabelle process terminated")
    1.52        for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
    1.53        system_result("process_manager terminated")