src/Pure/System/isabelle_process.scala
changeset 39572 bb3469024b6a
parent 39530 16adc476348f
child 39573 a874ca3f5474
     1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Sep 20 19:00:47 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Sep 20 21:20:06 2010 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4  
     1.5  import scala.actors.Actor
     1.6  import Actor._
     1.7 +import scala.collection.mutable
     1.8  
     1.9  
    1.10  object Isabelle_Process
    1.11 @@ -104,7 +105,8 @@
    1.12    private val stdin_writer =
    1.13      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
    1.14  
    1.15 -  Simple_Thread.actor("process_manager") {
    1.16 +  private val (process_manager, _) = Simple_Thread.actor("process_manager")
    1.17 +  {
    1.18      val (startup_failed, startup_output) =
    1.19      {
    1.20        val expired = System.currentTimeMillis() + timeout
    1.21 @@ -121,42 +123,50 @@
    1.22        }
    1.23        (!finished, result.toString)
    1.24      }
    1.25 +    system_result(startup_output)
    1.26 +
    1.27      if (startup_failed) {
    1.28 -      put_result(Markup.STDOUT, startup_output)
    1.29        put_result(Markup.EXIT, "127")
    1.30        stdin_writer.close
    1.31        Thread.sleep(300)  // FIXME !?
    1.32 -      proc.destroy  // FIXME reliable!?
    1.33 +      proc.destroy  // FIXME unreliable
    1.34      }
    1.35      else {
    1.36 -      put_result(Markup.SYSTEM, startup_output)
    1.37 -
    1.38 -      standard_input = stdin_actor()
    1.39 -      stdout_actor()
    1.40 -
    1.41        // rendezvous
    1.42        val command_stream = system.fifo_output_stream(in_fifo)
    1.43        val message_stream = system.fifo_input_stream(out_fifo)
    1.44  
    1.45 -      command_input = input_actor(command_stream)
    1.46 -      message_actor(message_stream)
    1.47 +      val stdin = stdin_actor(); standard_input = stdin._2
    1.48 +      val stdout = stdout_actor()
    1.49 +      val input = input_actor(command_stream); command_input = input._2
    1.50 +      val message = message_actor(message_stream)
    1.51  
    1.52        val rc = proc.waitFor()
    1.53 -      Thread.sleep(300)  // FIXME !?
    1.54        system_result("Isabelle process terminated")
    1.55 +      for ((thread, _) <- List(stdin, stdout, input, message)) thread.join
    1.56 +      system_result("process_manager terminated")
    1.57        put_result(Markup.EXIT, rc.toString)
    1.58      }
    1.59      rm_fifos()
    1.60    }
    1.61  
    1.62 +  def join() { process_manager.join() }
    1.63  
    1.64 -  /* results */
    1.65 +
    1.66 +  /* system log */
    1.67 +
    1.68 +  private val system_results = new mutable.ListBuffer[String]
    1.69  
    1.70    private def system_result(text: String)
    1.71    {
    1.72 +    synchronized { system_results += text }
    1.73      receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
    1.74    }
    1.75  
    1.76 +  def syslog(): List[String] = synchronized { system_results.toList }
    1.77 +
    1.78 +
    1.79 +  /* results */
    1.80  
    1.81    private val xml_cache = new XML.Cache(131071)
    1.82  
    1.83 @@ -219,7 +229,7 @@
    1.84  
    1.85    /* raw stdin */
    1.86  
    1.87 -  private def stdin_actor(): Actor =
    1.88 +  private def stdin_actor(): (Thread, Actor) =
    1.89    {
    1.90      val name = "standard_input"
    1.91      Simple_Thread.actor(name) {
    1.92 @@ -247,7 +257,7 @@
    1.93  
    1.94    /* raw stdout */
    1.95  
    1.96 -  private def stdout_actor(): Actor =
    1.97 +  private def stdout_actor(): (Thread, Actor) =
    1.98    {
    1.99      val name = "standard_output"
   1.100      Simple_Thread.actor(name) {
   1.101 @@ -283,7 +293,7 @@
   1.102  
   1.103    /* command input */
   1.104  
   1.105 -  private def input_actor(raw_stream: OutputStream): Actor =
   1.106 +  private def input_actor(raw_stream: OutputStream): (Thread, Actor) =
   1.107    {
   1.108      val name = "command_input"
   1.109      Simple_Thread.actor(name) {
   1.110 @@ -314,7 +324,7 @@
   1.111  
   1.112    /* message output */
   1.113  
   1.114 -  private def message_actor(stream: InputStream): Actor =
   1.115 +  private def message_actor(stream: InputStream): (Thread, Actor) =
   1.116    {
   1.117      class EOF extends Exception
   1.118      class Protocol_Error(msg: String) extends Exception(msg)