equal
deleted
inserted
replaced
1 /* Title: Tools/Graphview/src/mutator_event.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 Events for dialog synchronization. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import scala.collection.mutable |
|
13 |
|
14 import java.awt.Color |
|
15 |
|
16 |
|
17 object Mutator_Event |
|
18 { |
|
19 type Mutator_Markup = (Boolean, Color, Mutator) |
|
20 |
|
21 sealed abstract class Message |
|
22 case class Add(m: Mutator_Markup) extends Message |
|
23 case class NewList(m: List[Mutator_Markup]) extends Message |
|
24 |
|
25 type Receiver = PartialFunction[Message, Unit] |
|
26 |
|
27 class Bus |
|
28 { |
|
29 private val receivers = new mutable.ListBuffer[Receiver] |
|
30 |
|
31 def += (r: Receiver) { GUI_Thread.require {}; receivers += r } |
|
32 def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r } |
|
33 def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) } |
|
34 } |
|
35 } |
|