slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;
authorwenzelm
Sat Sep 18 17:14:47 2010 +0200 (2010-09-18 ago)
changeset 39519b376f53bcc18
parent 39518 96180281c3b2
child 39520 bad14b7d0520
slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/System/isabelle_process.scala	Sat Sep 18 17:11:39 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Sep 18 17:14:47 2010 +0200
     1.3 @@ -147,9 +147,13 @@
     1.4  
     1.5    /** stream actors **/
     1.6  
     1.7 -  case class Input_Text(text: String)
     1.8 -  case class Input_Chunks(chunks: List[Array[Byte]])
     1.9 -  case object Close
    1.10 +  private val in_fifo = system.mk_fifo()
    1.11 +  private val out_fifo = system.mk_fifo()
    1.12 +  private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
    1.13 +
    1.14 +  private case class Input_Text(text: String)
    1.15 +  private case class Input_Chunks(chunks: List[Array[Byte]])
    1.16 +  private case object Close
    1.17  
    1.18  
    1.19    /* raw stdin */
    1.20 @@ -220,9 +224,9 @@
    1.21  
    1.22    /* command input */
    1.23  
    1.24 -  private def input_actor(name: String, raw_stream: OutputStream): Actor =
    1.25 +  private def input_actor(name: String): Actor =
    1.26      Simple_Thread.actor(name) {
    1.27 -      val stream = new BufferedOutputStream(raw_stream)
    1.28 +      val stream = new BufferedOutputStream(system.fifo_output_stream(in_fifo))  // FIXME potentially blocking forever
    1.29        var finished = false
    1.30        while (!finished) {
    1.31          try {
    1.32 @@ -252,8 +256,9 @@
    1.33  
    1.34    private class Protocol_Error(msg: String) extends Exception(msg)
    1.35  
    1.36 -  private def message_actor(name: String, stream: InputStream): Actor =
    1.37 +  private def message_actor(name: String): Actor =
    1.38      Simple_Thread.actor(name) {
    1.39 +      val stream = system.fifo_input_stream(out_fifo)  // FIXME potentially blocking forever
    1.40        val default_buffer = new Array[Byte](65536)
    1.41        var c = -1
    1.42  
    1.43 @@ -317,10 +322,6 @@
    1.44  
    1.45    /* exec process */
    1.46  
    1.47 -  private val in_fifo = system.mk_fifo()
    1.48 -  private val out_fifo = system.mk_fifo()
    1.49 -  private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
    1.50 -
    1.51    try {
    1.52      val cmdline =
    1.53        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
    1.54 @@ -335,12 +336,12 @@
    1.55  
    1.56    /* I/O actors */
    1.57  
    1.58 +  private val command_input = input_actor("command_input")
    1.59 +  message_actor("message_output")
    1.60 +
    1.61    private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream)
    1.62    stdout_actor("standard_output", proc.get.getInputStream)
    1.63  
    1.64 -  private val command_input = input_actor("command_input", system.fifo_output_stream(in_fifo))
    1.65 -  message_actor("message_output", system.fifo_input_stream(out_fifo))
    1.66 -
    1.67  
    1.68    /* exit process */
    1.69