src/Pure/GUI/swing_thread.scala
changeset 56662 f373fb77e0a4
parent 55618 995162143ef4
child 56770 e160ae47db94
equal deleted inserted replaced
56661:ef623f6f036b 56662:f373fb77e0a4
    33 
    33 
    34   def now[A](body: => A): A =
    34   def now[A](body: => A): A =
    35   {
    35   {
    36     if (SwingUtilities.isEventDispatchThread()) body
    36     if (SwingUtilities.isEventDispatchThread()) body
    37     else {
    37     else {
    38       lazy val result = { assert(); Exn.capture(body) }
    38       lazy val result = { assert { Exn.capture(body) } }
    39       SwingUtilities.invokeAndWait(new Runnable { def run = result })
    39       SwingUtilities.invokeAndWait(new Runnable { def run = result })
    40       Exn.release(result)
    40       Exn.release(result)
    41     }
    41     }
    42   }
    42   }
    43 
    43 
    67     new Delay {
    67     new Delay {
    68       private val timer = new Timer(time.ms.toInt, null)
    68       private val timer = new Timer(time.ms.toInt, null)
    69       timer.setRepeats(false)
    69       timer.setRepeats(false)
    70       timer.addActionListener(new ActionListener {
    70       timer.addActionListener(new ActionListener {
    71         override def actionPerformed(e: ActionEvent) {
    71         override def actionPerformed(e: ActionEvent) {
    72           assert()
    72           assert {}
    73           timer.setInitialDelay(time.ms.toInt)
    73           timer.setInitialDelay(time.ms.toInt)
    74           action
    74           action
    75         }
    75         }
    76       })
    76       })
    77 
    77 
    78       def invoke()
    78       def invoke()
    79       {
    79       {
    80         require()
    80         require {}
    81         if (first) timer.start() else timer.restart()
    81         if (first) timer.start() else timer.restart()
    82       }
    82       }
    83 
    83 
    84       def revoke()
    84       def revoke()
    85       {
    85       {
    86         require()
    86         require {}
    87         timer.stop()
    87         timer.stop()
    88         timer.setInitialDelay(time.ms.toInt)
    88         timer.setInitialDelay(time.ms.toInt)
    89       }
    89       }
    90 
    90 
    91       def postpone(alt_time: Time)
    91       def postpone(alt_time: Time)
    92       {
    92       {
    93         require()
    93         require {}
    94         if (timer.isRunning) {
    94         if (timer.isRunning) {
    95           timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
    95           timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
    96           timer.restart()
    96           timer.restart()
    97         }
    97         }
    98       }
    98       }