# HG changeset patch
# User wenzelm
# Date 1252354336 -7200
# Node ID 668052c4220e48c3a2286625b597533a4cab9d49
# Parent  32e0c39df91d8627eded002651afdfa8b3b055d1
modernized Event_Bus -- based on actors;

diff -r 32e0c39df91d -r 668052c4220e src/Pure/General/event_bus.scala
--- a/src/Pure/General/event_bus.scala	Mon Sep 07 19:41:30 2009 +0200
+++ b/src/Pure/General/event_bus.scala	Mon Sep 07 22:12:16 2009 +0200
@@ -1,38 +1,35 @@
 /*  Title:      Pure/General/event_bus.scala
     Author:     Makarius
 
-Generic event bus with multiple handlers and optional exception
-logging.
+Generic event bus with multiple receiving actors.
 */
 
 package isabelle
 
+import scala.actors.Actor, Actor._
 import scala.collection.mutable.ListBuffer
 
 
-class EventBus[Event]
+class Event_Bus[Event]
 {
-  /* event handlers */
+  /* receivers */
+
+  private val receivers = new ListBuffer[Actor]
+
+  def += (r: Actor) { synchronized { receivers += r } }
+  def + (r: Actor): Event_Bus[Event] = { this += r; this }
 
-  type Handler = Event => Unit
-  private val handlers = new ListBuffer[Handler]
+  def += (f: Event => Unit) {
+    this += actor { loop { react { case x: Event => f(x) } } }
+  }
 
-  def += (h: Handler) = synchronized { handlers += h }
-  def + (h: Handler) = { this += h; this }
+  def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
 
-  def -= (h: Handler) = synchronized { handlers -= h }
-  def - (h: Handler) = { this -= h; this }
+  def -= (r: Actor) { synchronized { receivers -= r } }
+  def - (r: Actor) = { this -= r; this }
 
 
   /* event invocation */
 
-  var logger: Throwable => Unit = throw _
-
-  def event(x: Event) = {
-    val log = logger
-    for (h <- synchronized { handlers.toList }) {
-      try { h(x) }
-      catch { case e: Throwable => log(e) }
-    }
-  }
+  def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
 }
diff -r 32e0c39df91d -r 668052c4220e src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Sep 07 19:41:30 2009 +0200
+++ b/src/Pure/IsaMakefile	Mon Sep 07 22:12:16 2009 +0200
@@ -134,7 +134,7 @@
 
 $(FULL_JAR): $(SCALA_FILES)
 	@rm -rf classes && mkdir classes
-	"$(SCALA_HOME)/bin/scalac" -deprecation -d classes -target jvm-1.5 $(SCALA_FILES)
+	"$(SCALA_HOME)/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 $(SCALA_FILES)
 	"$(SCALA_HOME)/bin/scaladoc" -d classes $(SCALA_FILES)
 	@cp $(SCALA_FILES) classes/isabelle
 	@mkdir -p "$(JAR_DIR)"