src/Pure/System/isabelle_process.scala
changeset 45027 f459e93a038e
parent 44775 27930cf6f0f7
child 45055 55274f7e306b
     1.1 --- a/src/Pure/System/isabelle_process.scala	Wed Sep 21 17:50:25 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Sep 21 20:35:50 2011 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4  
     1.5    private def put_result(kind: String, props: Properties.T, body: XML.Body)
     1.6    {
     1.7 -    if (kind == Markup.INIT) rm_fifos()
     1.8 +    if (kind == Markup.INIT) system_channel.accepted()
     1.9      if (kind == Markup.RAW)
    1.10        receiver(new Result(XML.Elem(Markup(kind, props), body)))
    1.11      else {
    1.12 @@ -131,18 +131,16 @@
    1.13  
    1.14    /** process manager **/
    1.15  
    1.16 -  private val in_fifo = Isabelle_System.mk_fifo()
    1.17 -  private val out_fifo = Isabelle_System.mk_fifo()
    1.18 -  private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) }
    1.19 +  private val system_channel = System_Channel()
    1.20  
    1.21    private val process =
    1.22      try {
    1.23        val cmdline =
    1.24 -        List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W",
    1.25 -          in_fifo + ":" + out_fifo) ++ args
    1.26 +        Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
    1.27 +          (system_channel.isabelle_args ::: args.toList)
    1.28        new Isabelle_System.Managed_Process(true, cmdline: _*)
    1.29      }
    1.30 -    catch { case e: IOException => rm_fifos(); throw(e) }
    1.31 +    catch { case e: IOException => system_channel.accepted(); throw(e) }
    1.32  
    1.33    val process_result =
    1.34      Simple_Thread.future("process_result") { process.join }
    1.35 @@ -182,9 +180,7 @@
    1.36        process_result.join
    1.37      }
    1.38      else {
    1.39 -      // rendezvous
    1.40 -      val command_stream = Isabelle_System.fifo_output_stream(in_fifo)
    1.41 -      val message_stream = Isabelle_System.fifo_input_stream(out_fifo)
    1.42 +      val (command_stream, message_stream) = system_channel.rendezvous()
    1.43  
    1.44        standard_input = stdin_actor()
    1.45        val stdout = stdout_actor()
    1.46 @@ -197,7 +193,7 @@
    1.47        system_result("process_manager terminated")
    1.48        put_result(Markup.EXIT, "Return code: " + rc.toString)
    1.49      }
    1.50 -    rm_fifos()
    1.51 +    system_channel.accepted()
    1.52    }
    1.53  
    1.54