| author | wenzelm |
| Thu, 24 Jul 2014 10:38:46 +0200 | |
| changeset 57638 | ed58e740a699 |
| parent 57613 | 4c6d44a3a079 |
| child 61194 | e4699ef5cf90 |
| permissions | -rw-r--r-- |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56773
diff
changeset
|
1 |
/* Title: Pure/GUI/gui_thread.scala |
|
53853
e8430d668f44
more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material);
wenzelm
parents:
53783
diff
changeset
|
2 |
Module: PIDE-GUI |
| 29202 | 3 |
Author: Makarius |
4 |
||
| 57613 | 5 |
Evaluation within the GUI thread (for AWT/Swing). |
| 29202 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
| 55618 | 10 |
|
| 56773 | 11 |
import javax.swing.SwingUtilities |
|
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
12 |
|
| 29202 | 13 |
|
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56773
diff
changeset
|
14 |
object GUI_Thread |
| 29202 | 15 |
{
|
| 56773 | 16 |
/* context check */ |
| 32494 | 17 |
|
| 52859 | 18 |
def assert[A](body: => A) = |
19 |
{
|
|
20 |
Predef.assert(SwingUtilities.isEventDispatchThread()) |
|
21 |
body |
|
22 |
} |
|
| 32494 | 23 |
|
| 52859 | 24 |
def require[A](body: => A) = |
25 |
{
|
|
26 |
Predef.require(SwingUtilities.isEventDispatchThread()) |
|
27 |
body |
|
28 |
} |
|
| 52477 | 29 |
|
| 32494 | 30 |
|
| 56773 | 31 |
/* event dispatch queue */ |
|
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
32 |
|
| 34026 | 33 |
def now[A](body: => A): A = |
34 |
{
|
|
|
48000
880f1693299a
further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents:
47989
diff
changeset
|
35 |
if (SwingUtilities.isEventDispatchThread()) body |
|
880f1693299a
further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents:
47989
diff
changeset
|
36 |
else {
|
|
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
55618
diff
changeset
|
37 |
lazy val result = { assert { Exn.capture(body) } }
|
|
48000
880f1693299a
further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents:
47989
diff
changeset
|
38 |
SwingUtilities.invokeAndWait(new Runnable { def run = result })
|
|
880f1693299a
further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents:
47989
diff
changeset
|
39 |
Exn.release(result) |
|
880f1693299a
further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents:
47989
diff
changeset
|
40 |
} |
|
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
41 |
} |
| 29202 | 42 |
|
|
34299
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
43 |
def later(body: => Unit) |
|
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
44 |
{
|
| 32494 | 45 |
if (SwingUtilities.isEventDispatchThread()) body |
|
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
46 |
else SwingUtilities.invokeLater(new Runnable { def run = body })
|
|
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
47 |
} |
|
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 |
|
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56662
diff
changeset
|
50 |
/* delayed events */ |
| 49195 | 51 |
|
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56662
diff
changeset
|
52 |
def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay = |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56662
diff
changeset
|
53 |
Simple_Thread.delay_first(delay) { later { event } }
|
|
49196
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
54 |
|
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56662
diff
changeset
|
55 |
def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay = |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56662
diff
changeset
|
56 |
Simple_Thread.delay_last(delay) { later { event } }
|
| 29202 | 57 |
} |