1.1 --- a/src/Pure/System/isabelle_process.scala	Thu Apr 24 13:40:29 2014 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Apr 24 13:54:45 2014 +0200
     1.3 @@ -57,19 +57,19 @@
     1.4  
     1.5    /* command input actor */
     1.6  
     1.7 +  @volatile private var command_input: (Thread, Actor) = null
     1.8 +
     1.9    private case class Input_Chunks(chunks: List[Bytes])
    1.10  
    1.11    private case object Close
    1.12 -  private def close(p: (Thread, Actor))
    1.13 +  private def close_input()
    1.14    {
    1.15 -    if (p != null && p._1.isAlive) {
    1.16 -      p._2 ! Close
    1.17 -      p._1.join
    1.18 +    if (command_input != null && command_input._1.isAlive) {
    1.19 +      command_input._2 ! Close
    1.20 +      command_input._1.join
    1.21      }
    1.22    }
    1.23  
    1.24 -  @volatile private var command_input: (Thread, Actor) = null
    1.25 -
    1.26  
    1.27  
    1.28    /** process manager **/
    1.29 @@ -126,16 +126,16 @@
    1.30      else {
    1.31        val (command_stream, message_stream) = system_channel.rendezvous()
    1.32  
    1.33 -      val stdout = physical_output_actor(false)
    1.34 -      val stderr = physical_output_actor(true)
    1.35 +      val stdout = physical_output(false)
    1.36 +      val stderr = physical_output(true)
    1.37 +      val message = message_output(message_stream)
    1.38 +
    1.39        command_input = input_actor(command_stream)
    1.40 -      val message = message_actor(message_stream)
    1.41  
    1.42        val rc = process_result.join
    1.43        system_output("process terminated")
    1.44 -      close(command_input)
    1.45 -      for ((thread, _) <- List(stdout, stderr, command_input, message))
    1.46 -        thread.join
    1.47 +      close_input()
    1.48 +      for (thread <- List(stdout, stderr, message)) thread.join
    1.49        system_output("process_manager terminated")
    1.50        exit_message(rc)
    1.51      }
    1.52 @@ -155,7 +155,7 @@
    1.53  
    1.54    def terminate()
    1.55    {
    1.56 -    close(command_input)
    1.57 +    close_input()
    1.58      system_output("Terminating Isabelle process")
    1.59      terminate_process()
    1.60    }
    1.61 @@ -166,13 +166,13 @@
    1.62  
    1.63    /* physical output */
    1.64  
    1.65 -  private def physical_output_actor(err: Boolean): (Thread, Actor) =
    1.66 +  private def physical_output(err: Boolean): Thread =
    1.67    {
    1.68      val (name, reader, markup) =
    1.69        if (err) ("standard_error", process.stderr, Markup.STDERR)
    1.70        else ("standard_output", process.stdout, Markup.STDOUT)
    1.71  
    1.72 -    Simple_Thread.actor(name) {
    1.73 +    Simple_Thread.fork(name) {
    1.74        try {
    1.75          var result = new StringBuilder(100)
    1.76          var finished = false
    1.77 @@ -234,13 +234,13 @@
    1.78  
    1.79    /* message output */
    1.80  
    1.81 -  private def message_actor(stream: InputStream): (Thread, Actor) =
    1.82 +  private def message_output(stream: InputStream): Thread =
    1.83    {
    1.84      class EOF extends Exception
    1.85      class Protocol_Error(msg: String) extends Exception(msg)
    1.86  
    1.87      val name = "message_output"
    1.88 -    Simple_Thread.actor(name) {
    1.89 +    Simple_Thread.fork(name) {
    1.90        val default_buffer = new Array[Byte](65536)
    1.91        var c = -1
    1.92