src/Pure/General/swing.scala
author wenzelm
Wed, 28 Jan 2009 11:36:45 +0100
changeset 29649 8b0c1397868e
parent 29202 2454172eddae
child 29777 f3284860004c
permissions -rw-r--r--
more robust treatment of SwingUtilities.isEventDispatchThread;
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
{
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
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    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
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    22
}