src/Pure/General/swing_thread.scala
author wenzelm
Tue Jun 30 21:19:32 2009 +0200 (2009-06-30)
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;
wenzelm@31862
     1
/*  Title:      Pure/General/swing_thread.scala
wenzelm@29202
     2
    Author:     Makarius
wenzelm@29202
     3
wenzelm@31862
     4
Evaluation within the AWT/Swing thread.
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@31862
    11
object Swing_Thread
wenzelm@29202
    12
{
wenzelm@29777
    13
  def now[A](body: => A): A = {
wenzelm@29777
    14
    var result: Option[A] = None
wenzelm@29777
    15
    if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
wenzelm@29777
    16
    else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
wenzelm@29777
    17
    result.get
wenzelm@29649
    18
  }
wenzelm@29202
    19
wenzelm@29649
    20
  def later(body: => Unit) {
wenzelm@29649
    21
    if (SwingUtilities.isEventDispatchThread) body
wenzelm@29649
    22
    else SwingUtilities.invokeLater(new Runnable { def run = body })
wenzelm@29649
    23
  }
wenzelm@29202
    24
}