src/Pure/System/swing_thread.scala
changeset 36676 ac7961d42ac3
parent 34299 68716caa7745
child 38223 2a368e8e0a80
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/System/swing_thread.scala	Wed May 05 22:23:45 2010 +0200
     1.3 @@ -0,0 +1,63 @@
     1.4 +/*  Title:      Pure/System/swing_thread.scala
     1.5 +    Author:     Makarius
     1.6 +    Author:     Fabian Immler, TU Munich
     1.7 +
     1.8 +Evaluation within the AWT/Swing thread.
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +import javax.swing.{SwingUtilities, Timer}
    1.14 +import java.awt.event.{ActionListener, ActionEvent}
    1.15 +
    1.16 +
    1.17 +object Swing_Thread
    1.18 +{
    1.19 +  /* checks */
    1.20 +
    1.21 +  def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
    1.22 +  def require() = Predef.require(SwingUtilities.isEventDispatchThread())
    1.23 +
    1.24 +
    1.25 +  /* main dispatch queue */
    1.26 +
    1.27 +  def now[A](body: => A): A =
    1.28 +  {
    1.29 +    var result: Option[A] = None
    1.30 +    if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
    1.31 +    else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
    1.32 +    result.get
    1.33 +  }
    1.34 +
    1.35 +  def future[A](body: => A): Future[A] =
    1.36 +  {
    1.37 +    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
    1.38 +    else Future.fork { now(body) }
    1.39 +  }
    1.40 +
    1.41 +  def later(body: => Unit)
    1.42 +  {
    1.43 +    if (SwingUtilities.isEventDispatchThread()) body
    1.44 +    else SwingUtilities.invokeLater(new Runnable { def run = body })
    1.45 +  }
    1.46 +
    1.47 +
    1.48 +  /* delayed actions */
    1.49 +
    1.50 +  private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
    1.51 +  {
    1.52 +    val listener =
    1.53 +      new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
    1.54 +    val timer = new Timer(time_span, listener)
    1.55 +    timer.setRepeats(false)
    1.56 +
    1.57 +    def invoke() { if (first) timer.start() else timer.restart() }
    1.58 +    invoke _
    1.59 +  }
    1.60 +
    1.61 +  // delayed action after first invocation
    1.62 +  def delay_first = delayed_action(true) _
    1.63 +
    1.64 +  // delayed action after last invocation
    1.65 +  def delay_last = delayed_action(false) _
    1.66 +}