src/Pure/General/swing.scala
author wenzelm
Sun, 22 Feb 2009 20:37:18 +0100
changeset 29777 f3284860004c
parent 29649 8b0c1397868e
permissions -rw-r--r--
result for Swing.now;
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
{
29777
f3284860004c result for Swing.now;
wenzelm
parents: 29649
diff changeset
    13
  def now[A](body: => A): A = {
f3284860004c result for Swing.now;
wenzelm
parents: 29649
diff changeset
    14
    var result: Option[A] = None
f3284860004c result for Swing.now;
wenzelm
parents: 29649
diff changeset
    15
    if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
f3284860004c result for Swing.now;
wenzelm
parents: 29649
diff changeset
    16
    else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
f3284860004c result for Swing.now;
wenzelm
parents: 29649
diff changeset
    17
    result.get
29649
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    18
  }
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    19
29649
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    20
  def later(body: => Unit) {
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    21
    if (SwingUtilities.isEventDispatchThread) body
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    22
    else SwingUtilities.invokeLater(new Runnable { def run = body })
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    23
  }
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    24
}