1.1 --- a/src/Pure/System/isabelle_process.scala	Sat Sep 18 20:07:48 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Sep 18 21:10:07 2010 +0200
     1.3 @@ -147,10 +147,6 @@
     1.4  
     1.5    /** stream actors **/
     1.6  
     1.7 -  private val in_fifo = system.mk_fifo()
     1.8 -  private val out_fifo = system.mk_fifo()
     1.9 -  private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
    1.10 -
    1.11    private case class Input_Text(text: String)
    1.12    private case class Input_Chunks(chunks: List[Array[Byte]])
    1.13    private case object Close
    1.14 @@ -224,9 +220,9 @@
    1.15  
    1.16    /* command input */
    1.17  
    1.18 -  private def input_actor(name: String): Actor =
    1.19 +  private def input_actor(name: String, fifo: String): Actor =
    1.20      Simple_Thread.actor(name) {
    1.21 -      val stream = new BufferedOutputStream(system.fifo_output_stream(in_fifo))  // FIXME potentially blocking forever
    1.22 +      val stream = new BufferedOutputStream(system.fifo_output_stream(fifo))  // FIXME potentially blocking forever
    1.23        var finished = false
    1.24        while (!finished) {
    1.25          try {
    1.26 @@ -256,9 +252,9 @@
    1.27  
    1.28    private class Protocol_Error(msg: String) extends Exception(msg)
    1.29  
    1.30 -  private def message_actor(name: String): Actor =
    1.31 +  private def message_actor(name: String, fifo: String): Actor =
    1.32      Simple_Thread.actor(name) {
    1.33 -      val stream = system.fifo_input_stream(out_fifo)  // FIXME potentially blocking forever
    1.34 +      val stream = system.fifo_input_stream(fifo)  // FIXME potentially blocking forever
    1.35        val default_buffer = new Array[Byte](65536)
    1.36        var c = -1
    1.37  
    1.38 @@ -322,22 +318,22 @@
    1.39  
    1.40    /* exec process */
    1.41  
    1.42 +  private val in_fifo = system.mk_fifo()
    1.43 +  private val out_fifo = system.mk_fifo()
    1.44 +  private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
    1.45 +
    1.46    try {
    1.47      val cmdline =
    1.48        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
    1.49      proc = Some(system.execute(true, cmdline: _*))
    1.50    }
    1.51 -  catch {
    1.52 -    case e: IOException =>
    1.53 -      rm_fifos()
    1.54 -      error("Failed to execute Isabelle process: " + e.getMessage)
    1.55 -  }
    1.56 +  catch { case e: IOException => rm_fifos(); throw(e) }
    1.57  
    1.58  
    1.59    /* I/O actors */
    1.60  
    1.61 -  private val command_input = input_actor("command_input")
    1.62 -  message_actor("message_output")
    1.63 +  private val command_input = input_actor("command_input", in_fifo)
    1.64 +  message_actor("message_output", out_fifo)
    1.65  
    1.66    private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream)
    1.67    stdout_actor("standard_output", proc.get.getInputStream)
    1.68 @@ -351,7 +347,7 @@
    1.69        case Some(p) =>
    1.70          val rc = p.waitFor()
    1.71          Thread.sleep(300)  // FIXME property!?
    1.72 -        put_result(Markup.SYSTEM, "process_exit terminated")
    1.73 +        put_result(Markup.SYSTEM, "Isabelle process terminated")
    1.74          put_result(Markup.EXIT, rc.toString)
    1.75      }
    1.76      rm_fifos()