author | wenzelm |
Tue, 30 Jun 2009 21:19:32 +0200 | |
changeset 31862 | 53acb8ec6c51 |
parent 29777 | src/Pure/General/swing.scala@f3284860004c |
child 31942 | 63466160ff27 |
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 |
3 |
||
31862
53acb8ec6c51
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents:
29777
diff
changeset
|
4 |
Evaluation within the AWT/Swing thread. |
29202 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
import javax.swing.SwingUtilities |
|
10 |
||
31862
53acb8ec6c51
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents:
29777
diff
changeset
|
11 |
object Swing_Thread |
29202 | 12 |
{ |
29777 | 13 |
def now[A](body: => A): A = { |
14 |
var result: Option[A] = None |
|
15 |
if (SwingUtilities.isEventDispatchThread) { result = Some(body) } |
|
16 |
else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) |
|
17 |
result.get |
|
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
18 |
} |
29202 | 19 |
|
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
20 |
def later(body: => Unit) { |
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
21 |
if (SwingUtilities.isEventDispatchThread) body |
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
22 |
else SwingUtilities.invokeLater(new Runnable { def run = body }) |
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
23 |
} |
29202 | 24 |
} |