src/Pure/General/swing.scala
author blanchet
Tue, 17 Feb 2009 14:01:54 +0100
changeset 29956 62f931b257b7
parent 29649 8b0c1397868e
child 29777 f3284860004c
permissions -rw-r--r--
Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).
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
}