| author | haftmann |
| Tue, 03 Feb 2009 16:39:52 +0100 | |
| changeset 29782 | 02e76245e5af |
| parent 29649 | 8b0c1397868e |
| child 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 |
{
|
|
|
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
13 |
def now(body: => Unit) {
|
|
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
14 |
if (SwingUtilities.isEventDispatchThread) body |
|
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
15 |
else SwingUtilities.invokeAndWait(new Runnable { def run = body })
|
|
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
16 |
} |
| 29202 | 17 |
|
|
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
18 |
def later(body: => Unit) {
|
|
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
19 |
if (SwingUtilities.isEventDispatchThread) body |
|
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
20 |
else SwingUtilities.invokeLater(new Runnable { def run = body })
|
|
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
21 |
} |
| 29202 | 22 |
} |