src/Pure/General/swing.scala
author haftmann
Wed, 21 Jan 2009 23:40:23 +0100
changeset 29609 a010aab5bed0
parent 29202 2454172eddae
child 29649 8b0c1397868e
permissions -rw-r--r--
changed import hierarchy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/swing.scala
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     3
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     4
Swing utilities.
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     5
*/
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     6
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     7
package isabelle
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     8
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     9
import javax.swing.SwingUtilities
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    10
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    11
object Swing
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    12
{
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    13
  def now(body: => Unit) =
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    14
    SwingUtilities.invokeAndWait(new Runnable { def run = body })
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    15
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    16
  def later(body: => Unit) =
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    17
    SwingUtilities.invokeLater(new Runnable { def run = body })
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    18
}