author | wenzelm |
Fri, 07 Jun 2024 23:53:31 +0200 | |
changeset 80295 | 8a9588ffc133 |
parent 76709 | fdbdc573a06b |
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 |
|
75393 | 13 |
object GUI_Thread { |
56773 | 14 |
/* context check */ |
32494 | 15 |
|
76709 | 16 |
def check(): Boolean = SwingUtilities.isEventDispatchThread() |
17 |
||
75393 | 18 |
def assert[A](body: => A): A = { |
76709 | 19 |
Predef.assert(check()) |
52859 | 20 |
body |
21 |
} |
|
32494 | 22 |
|
75393 | 23 |
def require[A](body: => A): A = { |
76709 | 24 |
Predef.require(check(), "GUI thread expected") |
52859 | 25 |
body |
26 |
} |
|
52477 | 27 |
|
32494 | 28 |
|
56773 | 29 |
/* event dispatch queue */ |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
30 |
|
75393 | 31 |
def now[A](body: => A): A = { |
76709 | 32 |
if (check()) 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
|
33 |
else { |
71716 | 34 |
lazy val result = assert { Exn.capture(body) } |
35 |
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
|
36 |
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
|
37 |
} |
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
38 |
} |
29202 | 39 |
|
75393 | 40 |
def later(body: => Unit): Unit = { |
76709 | 41 |
if (check()) body |
71716 | 42 |
else SwingUtilities.invokeLater(() => body) |
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
43 |
} |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
44 |
|
75393 | 45 |
def future[A](body: => A): Future[A] = { |
76709 | 46 |
if (check()) 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
|
47 |
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
|
48 |
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
|
49 |
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
|
50 |
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
|
51 |
} |
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 |
} |
29202 | 53 |
} |