| author | huffman |
| Thu, 28 May 2009 14:36:21 -0700 | |
| changeset 31288 | 67dff9c5b2bd |
| parent 29777 | f3284860004c |
| 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 |
} |