src/Pure/System/swing_thread.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 48000 880f1693299a
child 49195 9d10bd85c1be
permissions -rw-r--r--
more official command specifications, including source position;
     1 /*  Title:      Pure/System/swing_thread.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4     Author:     Fabian Immler, TU Munich
     5 
     6 Evaluation within the AWT/Swing thread.
     7 */
     8 
     9 package isabelle
    10 
    11 import javax.swing.{SwingUtilities, Timer}
    12 import java.awt.event.{ActionListener, ActionEvent}
    13 
    14 
    15 object Swing_Thread
    16 {
    17   /* checks */
    18 
    19   def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
    20   def require() = Predef.require(SwingUtilities.isEventDispatchThread())
    21 
    22 
    23   /* main dispatch queue */
    24 
    25   def now[A](body: => A): A =
    26   {
    27     if (SwingUtilities.isEventDispatchThread()) body
    28     else {
    29       lazy val result = { assert(); Exn.capture(body) }
    30       SwingUtilities.invokeAndWait(new Runnable { def run = result })
    31       Exn.release(result)
    32     }
    33   }
    34 
    35   def future[A](body: => A): Future[A] =
    36   {
    37     if (SwingUtilities.isEventDispatchThread()) Future.value(body)
    38     else Future.fork { now(body) }
    39   }
    40 
    41   def later(body: => Unit)
    42   {
    43     if (SwingUtilities.isEventDispatchThread()) body
    44     else SwingUtilities.invokeLater(new Runnable { def run = body })
    45   }
    46 
    47 
    48   /* delayed actions */
    49 
    50   private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Boolean => Unit =
    51   {
    52     val listener = new ActionListener {
    53       override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
    54     }
    55     val timer = new Timer(time.ms.toInt, listener)
    56     timer.setRepeats(false)
    57 
    58     def invoke() { later { if (first) timer.start() else timer.restart() } }
    59     def revoke() { timer.stop() }
    60 
    61     (active: Boolean) => if (active) invoke() else revoke()
    62   }
    63 
    64   // delayed action after first invocation
    65   def delay_first = delayed_action(true) _
    66 
    67   // delayed action after last invocation
    68   def delay_last = delayed_action(false) _
    69 }