Isabelle_Process: receiver as Actor, not EventBus;
removed misleading Isabelle_Process.parse_message method -- use plain function instead;

--- a/src/Pure/Isar/isar.scala	Tue Sep 01 15:21:22 2009 +0200
+++ b/src/Pure/Isar/isar.scala	Tue Sep 01 21:03:04 2009 +0200
@@ -6,10 +6,11 @@
 
 package isabelle
 
+import scala.actors.Actor
 
-class Isar(isabelle_system: Isabelle_System,
-    results: EventBus[Isabelle_Process.Result], args: String*)
-  extends Isabelle_Process(isabelle_system, results, args: _*)
+
+class Isar(isabelle_system: Isabelle_System, receiver: Actor, args: String*)
+  extends Isabelle_Process(isabelle_system, receiver, args: _*)
 {
   /* basic editor commands */
 

--- a/src/Pure/System/isabelle_process.scala	Tue Sep 01 15:21:22 2009 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Sep 01 21:03:04 2009 +0200
@@ -11,9 +11,12 @@
 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
   InputStream, OutputStream, IOException}
 
+import scala.actors.Actor
+import Actor._
 
-object Isabelle_Process {
 
+object Isabelle_Process
+{
   /* results */
 
   object Kind extends Enumeration {
@@ -104,8 +107,7 @@
 }
 
 
-class Isabelle_Process(isabelle_system: Isabelle_System,
-  results: EventBus[Isabelle_Process.Result], args: String*)
+class Isabelle_Process(isabelle_system: Isabelle_System, receiver: Actor, args: String*)
 {
   import Isabelle_Process._
 
@@ -113,7 +115,8 @@
   /* demo constructor */
 
   def this(args: String*) =
-    this(new Isabelle_System, new EventBus[Isabelle_Process.Result] + Console.println, args: _*)
+    this(new Isabelle_System,
+      new Actor { def act = loop { react { case res => Console.println(res) } } }.start, args: _*)
 
 
   /* process information */
@@ -127,11 +130,6 @@
 
   /* results */
 
-  def parse_message(result: Result): XML.Tree =
-    Isabelle_Process.parse_message(isabelle_system, result)
-
-  private val result_queue = new LinkedBlockingQueue[Result]
-
   private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
   {
     if (kind == Kind.INIT) {
@@ -139,24 +137,7 @@
       if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
       if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
     }
-    result_queue.put(new Result(kind, props, result))
-  }
-
-  private class ResultThread extends Thread("isabelle: results") {
-    override def run() = {
-      var finished = false
-      while (!finished) {
-        val result =
-          try { result_queue.take }
-          catch { case _: NullPointerException => null }
-
-        if (result != null) {
-          results.event(result)
-          if (result.kind == Kind.EXIT) finished = true
-        }
-        else finished = true
-      }
-    }
+    receiver ! new Result(kind, props, result)
   }
 
 
@@ -396,8 +377,6 @@
     val message_thread = new MessageThread(message_fifo)
     message_thread.start
 
-    new ResultThread().start
-
 
     /* exec process */