# HG changeset patch
# User wenzelm
# Date 1285010406 -7200
# Node ID bb3469024b6a172e17483144e007f7dd127fdbf1
# Parent  3a3d9de2ad6ee51f4f52cfcafbcb0405bc264cf0
added Isabelle_Process.syslog;
refined Isabelle_Process.process_manager: startup_output via syslog, explicit join of auxiliary threads;
tuned;

diff -r 3a3d9de2ad6e -r bb3469024b6a src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Mon Sep 20 19:00:47 2010 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Mon Sep 20 21:20:06 2010 +0200
@@ -27,11 +27,11 @@
 
   /* thread as actor */
 
-  def actor(name: String, daemon: Boolean = false)(body: => Unit): Actor =
+  def actor(name: String, daemon: Boolean = false)(body: => Unit): (Thread, Actor) =
   {
     val actor = Future.promise[Actor]
     val thread = fork(name, daemon) { actor.fulfill(Actor.self); body }
-    actor.join
+    (thread, actor.join)
   }
 }
 
diff -r 3a3d9de2ad6e -r bb3469024b6a src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Sep 20 19:00:47 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Sep 20 21:20:06 2010 +0200
@@ -13,6 +13,7 @@
 
 import scala.actors.Actor
 import Actor._
+import scala.collection.mutable
 
 
 object Isabelle_Process
@@ -104,7 +105,8 @@
   private val stdin_writer =
     new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
 
-  Simple_Thread.actor("process_manager") {
+  private val (process_manager, _) = Simple_Thread.actor("process_manager")
+  {
     val (startup_failed, startup_output) =
     {
       val expired = System.currentTimeMillis() + timeout
@@ -121,42 +123,50 @@
       }
       (!finished, result.toString)
     }
+    system_result(startup_output)
+
     if (startup_failed) {
-      put_result(Markup.STDOUT, startup_output)
       put_result(Markup.EXIT, "127")
       stdin_writer.close
       Thread.sleep(300)  // FIXME !?
-      proc.destroy  // FIXME reliable!?
+      proc.destroy  // FIXME unreliable
     }
     else {
-      put_result(Markup.SYSTEM, startup_output)
-
-      standard_input = stdin_actor()
-      stdout_actor()
-
       // rendezvous
       val command_stream = system.fifo_output_stream(in_fifo)
       val message_stream = system.fifo_input_stream(out_fifo)
 
-      command_input = input_actor(command_stream)
-      message_actor(message_stream)
+      val stdin = stdin_actor(); standard_input = stdin._2
+      val stdout = stdout_actor()
+      val input = input_actor(command_stream); command_input = input._2
+      val message = message_actor(message_stream)
 
       val rc = proc.waitFor()
-      Thread.sleep(300)  // FIXME !?
       system_result("Isabelle process terminated")
+      for ((thread, _) <- List(stdin, stdout, input, message)) thread.join
+      system_result("process_manager terminated")
       put_result(Markup.EXIT, rc.toString)
     }
     rm_fifos()
   }
 
+  def join() { process_manager.join() }
 
-  /* results */
+
+  /* system log */
+
+  private val system_results = new mutable.ListBuffer[String]
 
   private def system_result(text: String)
   {
+    synchronized { system_results += text }
     receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
   }
 
+  def syslog(): List[String] = synchronized { system_results.toList }
+
+
+  /* results */
 
   private val xml_cache = new XML.Cache(131071)
 
@@ -219,7 +229,7 @@
 
   /* raw stdin */
 
-  private def stdin_actor(): Actor =
+  private def stdin_actor(): (Thread, Actor) =
   {
     val name = "standard_input"
     Simple_Thread.actor(name) {
@@ -247,7 +257,7 @@
 
   /* raw stdout */
 
-  private def stdout_actor(): Actor =
+  private def stdout_actor(): (Thread, Actor) =
   {
     val name = "standard_output"
     Simple_Thread.actor(name) {
@@ -283,7 +293,7 @@
 
   /* command input */
 
-  private def input_actor(raw_stream: OutputStream): Actor =
+  private def input_actor(raw_stream: OutputStream): (Thread, Actor) =
   {
     val name = "command_input"
     Simple_Thread.actor(name) {
@@ -314,7 +324,7 @@
 
   /* message output */
 
-  private def message_actor(stream: InputStream): Actor =
+  private def message_actor(stream: InputStream): (Thread, Actor) =
   {
     class EOF extends Exception
     class Protocol_Error(msg: String) extends Exception(msg)
diff -r 3a3d9de2ad6e -r bb3469024b6a src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Sep 20 19:00:47 2010 +0200
+++ b/src/Pure/System/session.scala	Mon Sep 20 21:20:06 2010 +0200
@@ -63,7 +63,8 @@
 
   private case object Stop
 
-  private val command_change_buffer = Simple_Thread.actor("command_change_buffer", daemon = true)
+  private val (_, command_change_buffer) =
+    Simple_Thread.actor("command_change_buffer", daemon = true)
   //{{{
   {
     import scala.compat.Platform.currentTime
@@ -118,7 +119,7 @@
   private case class Edit_Version(edits: List[Document.Node_Text_Edit])
   private case class Started(timeout: Int, args: List[String])
 
-  private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
+  private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
     var prover: Isabelle_Process with Isar_Document = null
 
@@ -202,7 +203,7 @@
           }
           else if (result.is_exit) prover = null  // FIXME ??
           else if (result.is_stdout) raw_output.event(result)
-          else if (!result.is_system) bad_result(result)  // FIXME syslog for system messages (!?)
+          else if (!result.is_system) bad_result(result)
         }
     }
     //}}}
@@ -216,7 +217,7 @@
       while (
         receiveWithin(0) {
           case result: Isabelle_Process.Result =>
-            if (result.is_stdout) {
+            if (result.is_system) {
               for (text <- XML.content(result.message))
                 buf.append(text)
             }
@@ -272,7 +273,7 @@
           if (prover == null) {
             prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
             val origin = sender
-            val opt_err = prover_startup(timeout)
+            val opt_err = prover_startup(timeout + 500)
             if (opt_err.isDefined) prover = null
             origin ! opt_err
           }