changeset 29202 | 2454172eddae |
child 29649 | 8b0c1397868e |
29201:03908107bc5b | 29202:2454172eddae |
---|---|
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 { |
|
13 def now(body: => Unit) = |
|
14 SwingUtilities.invokeAndWait(new Runnable { def run = body }) |
|
15 |
|
16 def later(body: => Unit) = |
|
17 SwingUtilities.invokeLater(new Runnable { def run = body }) |
|
18 } |