src/Pure/System/isabelle_process.scala
changeset 38253 3d4e521014f7
parent 38236 d8c7be27e01d
child 38259 2b61c5e27399
     1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Aug 09 13:56:02 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Aug 09 18:18:32 2010 +0200
     1.3 @@ -178,11 +178,14 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* stdin */
     1.8 +  /* commands */
     1.9  
    1.10 -  private class Stdin_Thread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
    1.11 -    override def run() = {
    1.12 -      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Standard_System.charset))
    1.13 +  private class Command_Thread(fifo: String) extends Thread("isabelle: commands")
    1.14 +  {
    1.15 +    override def run()
    1.16 +    {
    1.17 +      val stream = system.fifo_output_stream(fifo)
    1.18 +      val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
    1.19        var finished = false
    1.20        while (!finished) {
    1.21          try {
    1.22 @@ -200,19 +203,21 @@
    1.23            //}}}
    1.24          }
    1.25          catch {
    1.26 -          case e: IOException => put_result(Markup.SYSTEM, "Stdin thread: " + e.getMessage)
    1.27 +          case e: IOException => put_result(Markup.SYSTEM, "Command thread: " + e.getMessage)
    1.28          }
    1.29        }
    1.30 -      put_result(Markup.SYSTEM, "Stdin thread terminated")
    1.31 +      put_result(Markup.SYSTEM, "Command thread terminated")
    1.32      }
    1.33    }
    1.34  
    1.35  
    1.36 -  /* stdout */
    1.37 +  /* raw stdout */
    1.38  
    1.39 -  private class Stdout_Thread(in_stream: InputStream) extends Thread("isabelle: stdout") {
    1.40 -    override def run() = {
    1.41 -      val reader = new BufferedReader(new InputStreamReader(in_stream, Standard_System.charset))
    1.42 +  private class Stdout_Thread(stream: InputStream) extends Thread("isabelle: stdout")
    1.43 +  {
    1.44 +    override def run() =
    1.45 +    {
    1.46 +      val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
    1.47        var result = new StringBuilder(100)
    1.48  
    1.49        var finished = false
    1.50 @@ -253,7 +258,7 @@
    1.51      private class Protocol_Error(msg: String) extends Exception(msg)
    1.52      override def run()
    1.53      {
    1.54 -      val stream = system.fifo_stream(fifo)
    1.55 +      val stream = system.fifo_input_stream(fifo)
    1.56        val default_buffer = new Array[Byte](65536)
    1.57        var c = -1
    1.58  
    1.59 @@ -329,43 +334,44 @@
    1.60    /** main **/
    1.61  
    1.62    {
    1.63 -    /* messages */
    1.64 +    /* private communication channels */
    1.65  
    1.66 -    val message_fifo = system.mk_fifo()
    1.67 -    def rm_fifo() = system.rm_fifo(message_fifo)
    1.68 +    val in_fifo = system.mk_fifo()
    1.69 +    val out_fifo = system.mk_fifo()
    1.70 +    def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
    1.71  
    1.72 -    val message_thread = new Message_Thread(message_fifo)
    1.73 +    val command_thread = new Command_Thread(in_fifo)
    1.74 +    val message_thread = new Message_Thread(out_fifo)
    1.75 +
    1.76 +    command_thread.start
    1.77      message_thread.start
    1.78  
    1.79  
    1.80      /* exec process */
    1.81  
    1.82      try {
    1.83 -      val cmdline = List(system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
    1.84 +      val cmdline =
    1.85 +        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
    1.86        proc = system.execute(true, cmdline: _*)
    1.87      }
    1.88      catch {
    1.89        case e: IOException =>
    1.90 -        rm_fifo()
    1.91 +        rm_fifos()
    1.92          error("Failed to execute Isabelle process: " + e.getMessage)
    1.93      }
    1.94 -
    1.95 -
    1.96 -    /* stdin/stdout */
    1.97 -
    1.98 -    new Stdin_Thread(proc.getOutputStream).start
    1.99      new Stdout_Thread(proc.getInputStream).start
   1.100  
   1.101  
   1.102      /* exit */
   1.103  
   1.104      new Thread("isabelle: exit") {
   1.105 -      override def run() = {
   1.106 +      override def run()
   1.107 +      {
   1.108          val rc = proc.waitFor()
   1.109          Thread.sleep(300)  // FIXME property!?
   1.110          put_result(Markup.SYSTEM, "Exit thread terminated")
   1.111          put_result(Markup.EXIT, rc.toString)
   1.112 -        rm_fifo()
   1.113 +        rm_fifos()
   1.114        }
   1.115      }.start
   1.116    }