added Isabelle_Process.syslog;
authorwenzelm
Mon Sep 20 21:20:06 2010 +0200 (2010-09-20)
changeset 39572bb3469024b6a
parent 39571 3a3d9de2ad6e
child 39573 a874ca3f5474
added Isabelle_Process.syslog;
refined Isabelle_Process.process_manager: startup_output via syslog, explicit join of auxiliary threads;
tuned;
src/Pure/Concurrent/simple_thread.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/Concurrent/simple_thread.scala	Mon Sep 20 19:00:47 2010 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.scala	Mon Sep 20 21:20:06 2010 +0200
     1.3 @@ -27,11 +27,11 @@
     1.4  
     1.5    /* thread as actor */
     1.6  
     1.7 -  def actor(name: String, daemon: Boolean = false)(body: => Unit): Actor =
     1.8 +  def actor(name: String, daemon: Boolean = false)(body: => Unit): (Thread, Actor) =
     1.9    {
    1.10      val actor = Future.promise[Actor]
    1.11      val thread = fork(name, daemon) { actor.fulfill(Actor.self); body }
    1.12 -    actor.join
    1.13 +    (thread, actor.join)
    1.14    }
    1.15  }
    1.16  
     2.1 --- a/src/Pure/System/isabelle_process.scala	Mon Sep 20 19:00:47 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Sep 20 21:20:06 2010 +0200
     2.3 @@ -13,6 +13,7 @@
     2.4  
     2.5  import scala.actors.Actor
     2.6  import Actor._
     2.7 +import scala.collection.mutable
     2.8  
     2.9  
    2.10  object Isabelle_Process
    2.11 @@ -104,7 +105,8 @@
    2.12    private val stdin_writer =
    2.13      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
    2.14  
    2.15 -  Simple_Thread.actor("process_manager") {
    2.16 +  private val (process_manager, _) = Simple_Thread.actor("process_manager")
    2.17 +  {
    2.18      val (startup_failed, startup_output) =
    2.19      {
    2.20        val expired = System.currentTimeMillis() + timeout
    2.21 @@ -121,42 +123,50 @@
    2.22        }
    2.23        (!finished, result.toString)
    2.24      }
    2.25 +    system_result(startup_output)
    2.26 +
    2.27      if (startup_failed) {
    2.28 -      put_result(Markup.STDOUT, startup_output)
    2.29        put_result(Markup.EXIT, "127")
    2.30        stdin_writer.close
    2.31        Thread.sleep(300)  // FIXME !?
    2.32 -      proc.destroy  // FIXME reliable!?
    2.33 +      proc.destroy  // FIXME unreliable
    2.34      }
    2.35      else {
    2.36 -      put_result(Markup.SYSTEM, startup_output)
    2.37 -
    2.38 -      standard_input = stdin_actor()
    2.39 -      stdout_actor()
    2.40 -
    2.41        // rendezvous
    2.42        val command_stream = system.fifo_output_stream(in_fifo)
    2.43        val message_stream = system.fifo_input_stream(out_fifo)
    2.44  
    2.45 -      command_input = input_actor(command_stream)
    2.46 -      message_actor(message_stream)
    2.47 +      val stdin = stdin_actor(); standard_input = stdin._2
    2.48 +      val stdout = stdout_actor()
    2.49 +      val input = input_actor(command_stream); command_input = input._2
    2.50 +      val message = message_actor(message_stream)
    2.51  
    2.52        val rc = proc.waitFor()
    2.53 -      Thread.sleep(300)  // FIXME !?
    2.54        system_result("Isabelle process terminated")
    2.55 +      for ((thread, _) <- List(stdin, stdout, input, message)) thread.join
    2.56 +      system_result("process_manager terminated")
    2.57        put_result(Markup.EXIT, rc.toString)
    2.58      }
    2.59      rm_fifos()
    2.60    }
    2.61  
    2.62 +  def join() { process_manager.join() }
    2.63  
    2.64 -  /* results */
    2.65 +
    2.66 +  /* system log */
    2.67 +
    2.68 +  private val system_results = new mutable.ListBuffer[String]
    2.69  
    2.70    private def system_result(text: String)
    2.71    {
    2.72 +    synchronized { system_results += text }
    2.73      receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
    2.74    }
    2.75  
    2.76 +  def syslog(): List[String] = synchronized { system_results.toList }
    2.77 +
    2.78 +
    2.79 +  /* results */
    2.80  
    2.81    private val xml_cache = new XML.Cache(131071)
    2.82  
    2.83 @@ -219,7 +229,7 @@
    2.84  
    2.85    /* raw stdin */
    2.86  
    2.87 -  private def stdin_actor(): Actor =
    2.88 +  private def stdin_actor(): (Thread, Actor) =
    2.89    {
    2.90      val name = "standard_input"
    2.91      Simple_Thread.actor(name) {
    2.92 @@ -247,7 +257,7 @@
    2.93  
    2.94    /* raw stdout */
    2.95  
    2.96 -  private def stdout_actor(): Actor =
    2.97 +  private def stdout_actor(): (Thread, Actor) =
    2.98    {
    2.99      val name = "standard_output"
   2.100      Simple_Thread.actor(name) {
   2.101 @@ -283,7 +293,7 @@
   2.102  
   2.103    /* command input */
   2.104  
   2.105 -  private def input_actor(raw_stream: OutputStream): Actor =
   2.106 +  private def input_actor(raw_stream: OutputStream): (Thread, Actor) =
   2.107    {
   2.108      val name = "command_input"
   2.109      Simple_Thread.actor(name) {
   2.110 @@ -314,7 +324,7 @@
   2.111  
   2.112    /* message output */
   2.113  
   2.114 -  private def message_actor(stream: InputStream): Actor =
   2.115 +  private def message_actor(stream: InputStream): (Thread, Actor) =
   2.116    {
   2.117      class EOF extends Exception
   2.118      class Protocol_Error(msg: String) extends Exception(msg)
     3.1 --- a/src/Pure/System/session.scala	Mon Sep 20 19:00:47 2010 +0200
     3.2 +++ b/src/Pure/System/session.scala	Mon Sep 20 21:20:06 2010 +0200
     3.3 @@ -63,7 +63,8 @@
     3.4  
     3.5    private case object Stop
     3.6  
     3.7 -  private val command_change_buffer = Simple_Thread.actor("command_change_buffer", daemon = true)
     3.8 +  private val (_, command_change_buffer) =
     3.9 +    Simple_Thread.actor("command_change_buffer", daemon = true)
    3.10    //{{{
    3.11    {
    3.12      import scala.compat.Platform.currentTime
    3.13 @@ -118,7 +119,7 @@
    3.14    private case class Edit_Version(edits: List[Document.Node_Text_Edit])
    3.15    private case class Started(timeout: Int, args: List[String])
    3.16  
    3.17 -  private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
    3.18 +  private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    3.19    {
    3.20      var prover: Isabelle_Process with Isar_Document = null
    3.21  
    3.22 @@ -202,7 +203,7 @@
    3.23            }
    3.24            else if (result.is_exit) prover = null  // FIXME ??
    3.25            else if (result.is_stdout) raw_output.event(result)
    3.26 -          else if (!result.is_system) bad_result(result)  // FIXME syslog for system messages (!?)
    3.27 +          else if (!result.is_system) bad_result(result)
    3.28          }
    3.29      }
    3.30      //}}}
    3.31 @@ -216,7 +217,7 @@
    3.32        while (
    3.33          receiveWithin(0) {
    3.34            case result: Isabelle_Process.Result =>
    3.35 -            if (result.is_stdout) {
    3.36 +            if (result.is_system) {
    3.37                for (text <- XML.content(result.message))
    3.38                  buf.append(text)
    3.39              }
    3.40 @@ -272,7 +273,7 @@
    3.41            if (prover == null) {
    3.42              prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
    3.43              val origin = sender
    3.44 -            val opt_err = prover_startup(timeout)
    3.45 +            val opt_err = prover_startup(timeout + 500)
    3.46              if (opt_err.isDefined) prover = null
    3.47              origin ! opt_err
    3.48            }