# HG changeset patch
# User wenzelm
# Date 1315297624 -7200
# Node ID c58b69d888ac303b3adb70fe56d21205824c2dcd
# Parent  8f7b3a89fc15886a1729b2ab5b7168994125bdf6
more abstract receiver interface;

diff -r 8f7b3a89fc15 -r c58b69d888ac src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Sep 06 10:16:12 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Sep 06 10:27:04 2011 +0200
@@ -75,22 +75,21 @@
 }
 
 
-class Isabelle_Process(timeout: Time, receiver: Actor, args: String*)
+class Isabelle_Process(timeout: Time, receiver: Isabelle_Process.Message => Unit, args: String*)
 {
   import Isabelle_Process._
 
 
   /* demo constructor */
 
-  def this(args: String*) =
-    this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*)
+  def this(args: String*) = this(Time.seconds(10), Console.println(_), args: _*)
 
 
   /* results */
 
   private def system_result(text: String)
   {
-    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
+    receiver(new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
   private val xml_cache = new XML.Cache()
@@ -99,10 +98,10 @@
   {
     if (kind == Markup.INIT) rm_fifos()
     if (kind == Markup.RAW)
-      receiver ! new Result(XML.Elem(Markup(kind, props), body))
+      receiver(new Result(XML.Elem(Markup(kind, props), body)))
     else {
       val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
-      receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
+      receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
     }
   }
 
@@ -399,7 +398,7 @@
 
   def input(name: String, args: String*): Unit =
   {
-    receiver ! new Input(name, args.toList)
+    receiver(new Input(name, args.toList))
     input_bytes(name, args.map(Standard_System.string_bytes): _*)
   }
 
diff -r 8f7b3a89fc15 -r c58b69d888ac src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Sep 06 10:16:12 2011 +0200
+++ b/src/Pure/System/session.scala	Tue Sep 06 10:27:04 2011 +0200
@@ -145,6 +145,7 @@
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
     val this_actor = self
+    def receiver(msg: Isabelle_Process.Message) { this_actor ! msg }
     var prover: Option[Isabelle_Process with Isar_Document] = None
 
     var prune_next = System.currentTimeMillis() + prune_delay.ms
@@ -371,7 +372,7 @@
         case Start(timeout, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
-            prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
+            prover = Some(new Isabelle_Process(timeout, receiver _, args:_*) with Isar_Document)
           }
 
         case Stop =>