src/Pure/General/swing_thread.scala
author wenzelm
Tue, 30 Jun 2009 21:19:32 +0200
changeset 31862 53acb8ec6c51
parent 29777 src/Pure/General/swing.scala@f3284860004c
child 31942 63466160ff27
permissions -rw-r--r--
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31862
53acb8ec6c51 renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents: 29777
diff changeset
     1
/*  Title:      Pure/General/swing_thread.scala
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     3
31862
53acb8ec6c51 renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents: 29777
diff changeset
     4
Evaluation within the AWT/Swing thread.
29202
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
31862
53acb8ec6c51 renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents: 29777
diff changeset
    11
object Swing_Thread
29202
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
}