src/Pure/System/isabelle_process.scala
changeset 39530 16adc476348f
parent 39528 c01d89d18ff0
child 39572 bb3469024b6a
     1.1 --- a/src/Pure/System/isabelle_process.scala	Sun Sep 19 23:38:34 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Sep 20 11:38:14 2010 +0200
     1.3 @@ -133,8 +133,13 @@
     1.4  
     1.5        standard_input = stdin_actor()
     1.6        stdout_actor()
     1.7 -      command_input = input_actor()
     1.8 -      message_actor()
     1.9 +
    1.10 +      // rendezvous
    1.11 +      val command_stream = system.fifo_output_stream(in_fifo)
    1.12 +      val message_stream = system.fifo_input_stream(out_fifo)
    1.13 +
    1.14 +      command_input = input_actor(command_stream)
    1.15 +      message_actor(message_stream)
    1.16  
    1.17        val rc = proc.waitFor()
    1.18        Thread.sleep(300)  // FIXME !?
    1.19 @@ -158,6 +163,7 @@
    1.20    private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
    1.21    {
    1.22      if (pid.isEmpty && kind == Markup.INIT) {
    1.23 +      rm_fifos()
    1.24        props.find(_._1 == Markup.PID).map(_._1) match {
    1.25          case None => system_result("Bad Isabelle process initialization: missing pid")
    1.26          case p => pid = p
    1.27 @@ -277,11 +283,11 @@
    1.28  
    1.29    /* command input */
    1.30  
    1.31 -  private def input_actor(): Actor =
    1.32 +  private def input_actor(raw_stream: OutputStream): Actor =
    1.33    {
    1.34      val name = "command_input"
    1.35      Simple_Thread.actor(name) {
    1.36 -      val stream = new BufferedOutputStream(system.fifo_output_stream(in_fifo))
    1.37 +      val stream = new BufferedOutputStream(raw_stream)
    1.38        var finished = false
    1.39        while (!finished) {
    1.40          try {
    1.41 @@ -308,14 +314,13 @@
    1.42  
    1.43    /* message output */
    1.44  
    1.45 -  private def message_actor(): Actor =
    1.46 +  private def message_actor(stream: InputStream): Actor =
    1.47    {
    1.48      class EOF extends Exception
    1.49      class Protocol_Error(msg: String) extends Exception(msg)
    1.50  
    1.51      val name = "message_output"
    1.52      Simple_Thread.actor(name) {
    1.53 -      val stream = system.fifo_input_stream(out_fifo)
    1.54        val default_buffer = new Array[Byte](65536)
    1.55        var c = -1
    1.56