src/Pure/General/swing.scala
author wenzelm
Wed Jan 28 11:36:45 2009 +0100 (2009-01-28)
changeset 29649 8b0c1397868e
parent 29202 2454172eddae
child 29777 f3284860004c
permissions -rw-r--r--
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm@29202
     1
/*  Title:      Pure/General/swing.scala
wenzelm@29202
     2
    Author:     Makarius
wenzelm@29202
     3
wenzelm@29202
     4
Swing utilities.
wenzelm@29202
     5
*/
wenzelm@29202
     6
wenzelm@29202
     7
package isabelle
wenzelm@29202
     8
wenzelm@29202
     9
import javax.swing.SwingUtilities
wenzelm@29202
    10
wenzelm@29202
    11
object Swing
wenzelm@29202
    12
{
wenzelm@29649
    13
  def now(body: => Unit) {
wenzelm@29649
    14
    if (SwingUtilities.isEventDispatchThread) body
wenzelm@29649
    15
    else SwingUtilities.invokeAndWait(new Runnable { def run = body })
wenzelm@29649
    16
  }
wenzelm@29202
    17
wenzelm@29649
    18
  def later(body: => Unit) {
wenzelm@29649
    19
    if (SwingUtilities.isEventDispatchThread) body
wenzelm@29649
    20
    else SwingUtilities.invokeLater(new Runnable { def run = body })
wenzelm@29649
    21
  }
wenzelm@29202
    22
}