author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73340 | 0ffcad1f6130 |
child 78615 | abdf38ee314a |
permissions | -rw-r--r-- |
59202 | 1 |
/* Title: Tools/Graphview/mutator_event.scala |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Markus Kaiser, TU Muenchen |
59240 | 3 |
Author: Makarius |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
5 |
Events for dialog synchronization. |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
6 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
7 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
8 |
package isabelle.graphview |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
9 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
10 |
|
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
11 |
import isabelle._ |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
12 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
13 |
|
75393 | 14 |
object Mutator_Event { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
sealed abstract class Message |
59221 | 16 |
case class Add(m: Mutator.Info) extends Message |
17 |
case class New_List(m: List[Mutator.Info]) extends Message |
|
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
18 |
|
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
19 |
type Receiver = PartialFunction[Message, Unit] |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
20 |
|
75393 | 21 |
class Bus { |
61590 | 22 |
private val receivers = Synchronized[List[Receiver]](Nil) |
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
23 |
|
73340 | 24 |
def += (r: Receiver): Unit = receivers.change(Library.insert(r)) |
25 |
def -= (r: Receiver): Unit = receivers.change(Library.remove(r)) |
|
26 |
def event(x: Message): Unit = receivers.value.reverse.foreach(r => r(x)) |
|
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
27 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
28 |
} |