# HG changeset patch
# User wenzelm
# Date 1281906836 -7200
# Node ID c13c95c97e899978bf533990eee8d5d72088c6ca
# Parent  7066fbd315ae510f1976fbf788e37e3eb2b32e69
event_bus.scala rather belongs to system plumbing;

diff -r 7066fbd315ae -r c13c95c97e89 src/Pure/PIDE/event_bus.scala
--- a/src/Pure/PIDE/event_bus.scala	Sun Aug 15 23:07:22 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-/*  Title:      Pure/PIDE/event_bus.scala
-    Author:     Makarius
-
-Generic event bus with multiple receiving actors.
-*/
-
-package isabelle
-
-import scala.actors.Actor, Actor._
-import scala.collection.mutable.ListBuffer
-
-
-class Event_Bus[Event]
-{
-  /* receivers */
-
-  private val receivers = new ListBuffer[Actor]
-
-  def += (r: Actor) { synchronized { receivers += r } }
-  def + (r: Actor): Event_Bus[Event] = { this += r; this }
-
-  def += (f: Event => Unit) {
-    this += actor { loop { react { case x: Event => f(x) } } }
-  }
-
-  def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
-
-  def -= (r: Actor) { synchronized { receivers -= r } }
-  def - (r: Actor) = { this -= r; this }
-
-
-  /* event invocation */
-
-  def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
-}
diff -r 7066fbd315ae -r c13c95c97e89 src/Pure/System/event_bus.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/event_bus.scala	Sun Aug 15 23:13:56 2010 +0200
@@ -0,0 +1,35 @@
+/*  Title:      Pure/System/event_bus.scala
+    Author:     Makarius
+
+Generic event bus with multiple receiving actors.
+*/
+
+package isabelle
+
+import scala.actors.Actor, Actor._
+import scala.collection.mutable.ListBuffer
+
+
+class Event_Bus[Event]
+{
+  /* receivers */
+
+  private val receivers = new ListBuffer[Actor]
+
+  def += (r: Actor) { synchronized { receivers += r } }
+  def + (r: Actor): Event_Bus[Event] = { this += r; this }
+
+  def += (f: Event => Unit) {
+    this += actor { loop { react { case x: Event => f(x) } } }
+  }
+
+  def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
+
+  def -= (r: Actor) { synchronized { receivers -= r } }
+  def - (r: Actor) = { this -= r; this }
+
+
+  /* event invocation */
+
+  def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
+}
diff -r 7066fbd315ae -r c13c95c97e89 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Aug 15 23:07:22 2010 +0200
+++ b/src/Pure/build-jars	Sun Aug 15 23:13:56 2010 +0200
@@ -39,11 +39,11 @@
   Isar/token.scala
   PIDE/command.scala
   PIDE/document.scala
-  PIDE/event_bus.scala
   PIDE/markup_node.scala
   PIDE/text.scala
   System/cygwin.scala
   System/download.scala
+  System/event_bus.scala
   System/gui_setup.scala
   System/isabelle_process.scala
   System/isabelle_syntax.scala