| author | wenzelm |
| Wed, 11 Nov 2020 21:00:14 +0100 | |
| changeset 72574 | d892f6d66402 |
| parent 71716 | d1538d4de057 |
| child 73120 | c3589f2dff31 |
| 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 |
| 29202 | 2 |
Author: Makarius |
3 |
||
| 57613 | 4 |
Evaluation within the GUI thread (for AWT/Swing). |
| 29202 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
| 55618 | 9 |
|
| 56773 | 10 |
import javax.swing.SwingUtilities |
|
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
11 |
|
| 29202 | 12 |
|
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56773
diff
changeset
|
13 |
object GUI_Thread |
| 29202 | 14 |
{
|
| 56773 | 15 |
/* context check */ |
| 32494 | 16 |
|
| 66094 | 17 |
def assert[A](body: => A): A = |
| 52859 | 18 |
{
|
| 71716 | 19 |
Predef.assert(SwingUtilities.isEventDispatchThread) |
| 52859 | 20 |
body |
21 |
} |
|
| 32494 | 22 |
|
| 66094 | 23 |
def require[A](body: => A): A = |
| 52859 | 24 |
{
|
| 71716 | 25 |
Predef.require(SwingUtilities.isEventDispatchThread) |
| 52859 | 26 |
body |
27 |
} |
|
| 52477 | 28 |
|
| 32494 | 29 |
|
| 56773 | 30 |
/* event dispatch queue */ |
|
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
31 |
|
| 34026 | 32 |
def now[A](body: => A): A = |
33 |
{
|
|
| 71716 | 34 |
if (SwingUtilities.isEventDispatchThread) 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
|
35 |
else {
|
| 71716 | 36 |
lazy val result = assert { Exn.capture(body) }
|
37 |
SwingUtilities.invokeAndWait(() => result) |
|
|
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 |
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
|
39 |
} |
|
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
40 |
} |
| 29202 | 41 |
|
|
34299
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
42 |
def later(body: => Unit) |
|
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
43 |
{
|
| 71716 | 44 |
if (SwingUtilities.isEventDispatchThread) body |
45 |
else SwingUtilities.invokeLater(() => body) |
|
|
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
46 |
} |
|
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
47 |
|
|
67129
0262a378d5d6
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents:
66094
diff
changeset
|
48 |
def future[A](body: => A): Future[A] = |
|
0262a378d5d6
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents:
66094
diff
changeset
|
49 |
{
|
| 71716 | 50 |
if (SwingUtilities.isEventDispatchThread) Future.value(body) |
|
67129
0262a378d5d6
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents:
66094
diff
changeset
|
51 |
else {
|
|
0262a378d5d6
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents:
66094
diff
changeset
|
52 |
val promise = Future.promise[A] |
|
0262a378d5d6
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents:
66094
diff
changeset
|
53 |
later { promise.fulfill_result(Exn.capture(body)) }
|
|
0262a378d5d6
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents:
66094
diff
changeset
|
54 |
promise |
|
0262a378d5d6
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents:
66094
diff
changeset
|
55 |
} |
|
0262a378d5d6
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;
wenzelm
parents:
66094
diff
changeset
|
56 |
} |
| 29202 | 57 |
} |