author | wenzelm |
Tue, 30 Dec 2014 14:11:06 +0100 | |
changeset 59202 | 711c2446dc9d |
parent 57612 | src/Tools/Graphview/src/mutator_event.scala@990ffb84489b |
child 59221 | f779f83ef4ec |
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 |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
3 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
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
|
5 |
*/ |
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 |
package isabelle.graphview |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
8 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
9 |
|
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
10 |
import isabelle._ |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
11 |
|
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
12 |
import scala.collection.mutable |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
13 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
14 |
import java.awt.Color |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
16 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
17 |
object Mutator_Event |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
18 |
{ |
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49557
diff
changeset
|
19 |
type Mutator_Markup = (Boolean, Color, Mutator) |
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
20 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
21 |
sealed abstract class Message |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
22 |
case class Add(m: Mutator_Markup) extends Message |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
23 |
case class NewList(m: List[Mutator_Markup]) extends Message |
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
24 |
|
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
25 |
type Receiver = PartialFunction[Message, Unit] |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
26 |
|
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
27 |
class Bus |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
28 |
{ |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
29 |
private val receivers = new mutable.ListBuffer[Receiver] |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
30 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56662
diff
changeset
|
31 |
def += (r: Receiver) { GUI_Thread.require {}; receivers += r } |
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56662
diff
changeset
|
32 |
def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r } |
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56662
diff
changeset
|
33 |
def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) } |
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
34 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
35 |
} |