equal
deleted
inserted
replaced
1 /* Title: Pure/PIDE/event_bus.scala |
|
2 Author: Makarius |
|
3 |
|
4 Generic event bus with multiple receiving actors. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 import scala.actors.Actor, Actor._ |
|
10 import scala.collection.mutable.ListBuffer |
|
11 |
|
12 |
|
13 class Event_Bus[Event] |
|
14 { |
|
15 /* receivers */ |
|
16 |
|
17 private val receivers = new ListBuffer[Actor] |
|
18 |
|
19 def += (r: Actor) { synchronized { receivers += r } } |
|
20 def + (r: Actor): Event_Bus[Event] = { this += r; this } |
|
21 |
|
22 def += (f: Event => Unit) { |
|
23 this += actor { loop { react { case x: Event => f(x) } } } |
|
24 } |
|
25 |
|
26 def + (f: Event => Unit): Event_Bus[Event] = { this += f; this } |
|
27 |
|
28 def -= (r: Actor) { synchronized { receivers -= r } } |
|
29 def - (r: Actor) = { this -= r; this } |
|
30 |
|
31 |
|
32 /* event invocation */ |
|
33 |
|
34 def event(x: Event) { synchronized { receivers.foreach(_ ! x) } } |
|
35 } |
|