author | huffman |
Tue, 02 Mar 2010 09:54:50 -0800 | |
changeset 35512 | d1ef88d7de5a |
parent 34299 | 68716caa7745 |
permissions | -rw-r--r-- |
31862
53acb8ec6c51
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents:
29777
diff
changeset
|
1 |
/* Title: Pure/General/swing_thread.scala |
29202 | 2 |
Author: Makarius |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
3 |
Author: Fabian Immler, TU Munich |
29202 | 4 |
|
31862
53acb8ec6c51
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents:
29777
diff
changeset
|
5 |
Evaluation within the AWT/Swing thread. |
29202 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
10 |
import javax.swing.{SwingUtilities, Timer} |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
11 |
import java.awt.event.{ActionListener, ActionEvent} |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
12 |
|
29202 | 13 |
|
31862
53acb8ec6c51
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents:
29777
diff
changeset
|
14 |
object Swing_Thread |
29202 | 15 |
{ |
32494 | 16 |
/* checks */ |
17 |
||
18 |
def assert() = Predef.assert(SwingUtilities.isEventDispatchThread()) |
|
19 |
def require() = Predef.require(SwingUtilities.isEventDispatchThread()) |
|
20 |
||
21 |
||
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
22 |
/* main dispatch queue */ |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
23 |
|
34026 | 24 |
def now[A](body: => A): A = |
25 |
{ |
|
29777 | 26 |
var result: Option[A] = None |
32494 | 27 |
if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } |
29777 | 28 |
else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) |
29 |
result.get |
|
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
30 |
} |
29202 | 31 |
|
34299
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
32 |
def future[A](body: => A): Future[A] = |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
33 |
{ |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
34 |
if (SwingUtilities.isEventDispatchThread()) Future.value(body) |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
35 |
else Future.fork { now(body) } |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
36 |
} |
34026 | 37 |
|
34299
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
38 |
def later(body: => Unit) |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
39 |
{ |
32494 | 40 |
if (SwingUtilities.isEventDispatchThread()) body |
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
41 |
else SwingUtilities.invokeLater(new Runnable { def run = body }) |
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
42 |
} |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
43 |
|
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
44 |
|
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
45 |
/* delayed actions */ |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
46 |
|
32501 | 47 |
private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit = |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
48 |
{ |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
49 |
val listener = |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
50 |
new ActionListener { override def actionPerformed(e: ActionEvent) { action } } |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
51 |
val timer = new Timer(time_span, listener) |
32501 | 52 |
timer.setRepeats(false) |
53 |
||
54 |
def invoke() { if (first) timer.start() else timer.restart() } |
|
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
55 |
invoke _ |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
56 |
} |
32501 | 57 |
|
58 |
// delayed action after first invocation |
|
59 |
def delay_first = delayed_action(true) _ |
|
60 |
||
61 |
// delayed action after last invocation |
|
62 |
def delay_last = delayed_action(false) _ |
|
29202 | 63 |
} |