src/Pure/General/swing_thread.scala
changeset 32494 4ab2292e452a
parent 31942 63466160ff27
child 32501 41aa620885c2
equal deleted inserted replaced
32493:457ea5ddbb9b 32494:4ab2292e452a
    11 import java.awt.event.{ActionListener, ActionEvent}
    11 import java.awt.event.{ActionListener, ActionEvent}
    12 
    12 
    13 
    13 
    14 object Swing_Thread
    14 object Swing_Thread
    15 {
    15 {
       
    16   /* checks */
       
    17 
       
    18   def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
       
    19   def require() = Predef.require(SwingUtilities.isEventDispatchThread())
       
    20 
       
    21 
    16   /* main dispatch queue */
    22   /* main dispatch queue */
    17 
    23 
    18   def now[A](body: => A): A = {
    24   def now[A](body: => A): A = {
    19     var result: Option[A] = None
    25     var result: Option[A] = None
    20     if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
    26     if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
    21     else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
    27     else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
    22     result.get
    28     result.get
    23   }
    29   }
    24 
    30 
    25   def later(body: => Unit) {
    31   def later(body: => Unit) {
    26     if (SwingUtilities.isEventDispatchThread) body
    32     if (SwingUtilities.isEventDispatchThread()) body
    27     else SwingUtilities.invokeLater(new Runnable { def run = body })
    33     else SwingUtilities.invokeLater(new Runnable { def run = body })
    28   }
    34   }
    29 
    35 
    30 
    36 
    31   /* delayed actions */
    37   /* delayed actions */