author | wenzelm |
Sun, 22 Feb 2009 20:37:18 +0100 | |
changeset 29777 | f3284860004c |
parent 29649 | 8b0c1397868e |
permissions | -rw-r--r-- |
29202 | 1 |
/* Title: Pure/General/swing.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Swing utilities. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
import javax.swing.SwingUtilities |
|
10 |
||
11 |
object Swing |
|
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 |
} |