author | wenzelm |
Thu, 24 May 2012 17:42:47 +0200 | |
changeset 47989 | 1e790c27162d |
parent 46740 | 852baa599351 |
child 48000 | 880f1693299a |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/System/swing_thread.scala |
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset
|
2 |
Module: PIDE |
29202 | 3 |
Author: Makarius |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
4 |
Author: Fabian Immler, TU Munich |
29202 | 5 |
|
31862
53acb8ec6c51
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents:
29777
diff
changeset
|
6 |
Evaluation within the AWT/Swing thread. |
29202 | 7 |
*/ |
8 |
||
9 |
package isabelle |
|
10 |
||
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
11 |
import javax.swing.{SwingUtilities, Timer} |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
12 |
import java.awt.event.{ActionListener, ActionEvent} |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
13 |
|
29202 | 14 |
|
31862
53acb8ec6c51
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents:
29777
diff
changeset
|
15 |
object Swing_Thread |
29202 | 16 |
{ |
32494 | 17 |
/* checks */ |
18 |
||
19 |
def assert() = Predef.assert(SwingUtilities.isEventDispatchThread()) |
|
20 |
def require() = Predef.require(SwingUtilities.isEventDispatchThread()) |
|
21 |
||
22 |
||
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
23 |
/* main dispatch queue */ |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
24 |
|
34026 | 25 |
def now[A](body: => A): A = |
26 |
{ |
|
47989
1e790c27162d
more robust Swing_Thread.now: allow body to fail;
wenzelm
parents:
46740
diff
changeset
|
27 |
@volatile var result: Option[Exn.Result[A]] = None |
1e790c27162d
more robust Swing_Thread.now: allow body to fail;
wenzelm
parents:
46740
diff
changeset
|
28 |
if (SwingUtilities.isEventDispatchThread()) { result = Some(Exn.capture(body)) } |
1e790c27162d
more robust Swing_Thread.now: allow body to fail;
wenzelm
parents:
46740
diff
changeset
|
29 |
else |
1e790c27162d
more robust Swing_Thread.now: allow body to fail;
wenzelm
parents:
46740
diff
changeset
|
30 |
SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(Exn.capture(body)) } }) |
1e790c27162d
more robust Swing_Thread.now: allow body to fail;
wenzelm
parents:
46740
diff
changeset
|
31 |
Exn.release(result.get) |
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
32 |
} |
29202 | 33 |
|
34299
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
34 |
def future[A](body: => A): Future[A] = |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
35 |
{ |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
36 |
if (SwingUtilities.isEventDispatchThread()) Future.value(body) |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
37 |
else Future.fork { now(body) } |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
38 |
} |
34026 | 39 |
|
34299
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
40 |
def later(body: => Unit) |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
41 |
{ |
32494 | 42 |
if (SwingUtilities.isEventDispatchThread()) body |
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
43 |
else SwingUtilities.invokeLater(new Runnable { def run = body }) |
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
44 |
} |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
45 |
|
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
46 |
|
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
47 |
/* delayed actions */ |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
48 |
|
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46574
diff
changeset
|
49 |
private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Boolean => Unit = |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
50 |
{ |
38223 | 51 |
val listener = new ActionListener { |
52 |
override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action } |
|
53 |
} |
|
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
38847
diff
changeset
|
54 |
val timer = new Timer(time.ms.toInt, listener) |
32501 | 55 |
timer.setRepeats(false) |
56 |
||
46574
41701fce8ac7
invoke later to reduce chance of causing deadlock;
wenzelm
parents:
45673
diff
changeset
|
57 |
def invoke() { later { if (first) timer.start() else timer.restart() } } |
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46574
diff
changeset
|
58 |
def revoke() { timer.stop() } |
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46574
diff
changeset
|
59 |
|
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46574
diff
changeset
|
60 |
(active: Boolean) => if (active) invoke() else revoke() |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
61 |
} |
32501 | 62 |
|
63 |
// delayed action after first invocation |
|
64 |
def delay_first = delayed_action(true) _ |
|
65 |
||
66 |
// delayed action after last invocation |
|
67 |
def delay_last = delayed_action(false) _ |
|
29202 | 68 |
} |