| author | wenzelm | 
| Tue, 25 Mar 2014 14:52:35 +0100 | |
| changeset 56276 | 9e2d5e3debd3 | 
| parent 55618 | 995162143ef4 | 
| child 56686 | 2386d1a3ca8f | 
| permissions | -rw-r--r-- | 
| 38428 
c13c95c97e89
event_bus.scala rather belongs to system plumbing;
 wenzelm parents: 
36676diff
changeset | 1 | /* Title: Pure/System/event_bus.scala | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45667diff
changeset | 2 | Module: PIDE | 
| 29190 | 3 | Author: Makarius | 
| 4 | ||
| 32539 | 5 | Generic event bus with multiple receiving actors. | 
| 29190 | 6 | */ | 
| 7 | ||
| 8 | package isabelle | |
| 9 | ||
| 55618 | 10 | |
| 32539 | 11 | import scala.actors.Actor, Actor._ | 
| 29191 | 12 | import scala.collection.mutable.ListBuffer | 
| 29190 | 13 | |
| 14 | ||
| 32539 | 15 | class Event_Bus[Event] | 
| 29200 | 16 | {
 | 
| 32539 | 17 | /* receivers */ | 
| 18 | ||
| 19 | private val receivers = new ListBuffer[Actor] | |
| 20 | ||
| 21 |   def += (r: Actor) { synchronized { receivers += r } }
 | |
| 22 |   def + (r: Actor): Event_Bus[Event] = { this += r; this }
 | |
| 29200 | 23 | |
| 32539 | 24 |   def += (f: Event => Unit) {
 | 
| 43406 
40c67d894be4
avoid compiler warning -- this is unchecked anyway;
 wenzelm parents: 
38849diff
changeset | 25 |     this += actor { loop { react { case x => f(x.asInstanceOf[Event]) } } }
 | 
| 32539 | 26 | } | 
| 29190 | 27 | |
| 32539 | 28 |   def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
 | 
| 29191 | 29 | |
| 32539 | 30 |   def -= (r: Actor) { synchronized { receivers -= r } }
 | 
| 31 |   def - (r: Actor) = { this -= r; this }
 | |
| 29190 | 32 | |
| 29200 | 33 | |
| 34 | /* event invocation */ | |
| 35 | ||
| 32539 | 36 |   def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
 | 
| 29190 | 37 | } |