--- a/src/Pure/General/event_bus.scala Mon Sep 07 22:08:05 2009 +0200
+++ b/src/Pure/General/event_bus.scala Mon Sep 07 22:13:32 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) } }
}
--- a/src/Pure/IsaMakefile Mon Sep 07 22:08:05 2009 +0200
+++ b/src/Pure/IsaMakefile Mon Sep 07 22:13:32 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)"