src/Pure/System/swing_thread.scala
author wenzelm
Sat Aug 07 16:15:52 2010 +0200 (2010-08-07)
changeset 38223 2a368e8e0a80
parent 36676 ac7961d42ac3
child 38847 57043221eb43
permissions -rw-r--r--
more explicit treatment of Swing thread context;
Document_Model.snapshot: require Swing thread;
     1 /*  Title:      Pure/System/swing_thread.scala
     2     Author:     Makarius
     3     Author:     Fabian Immler, TU Munich
     4 
     5 Evaluation within the AWT/Swing thread.
     6 */
     7 
     8 package isabelle
     9 
    10 import javax.swing.{SwingUtilities, Timer}
    11 import java.awt.event.{ActionListener, ActionEvent}
    12 
    13 
    14 object Swing_Thread
    15 {
    16   /* checks */
    17 
    18   def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
    19   def require() = Predef.require(SwingUtilities.isEventDispatchThread())
    20 
    21 
    22   /* main dispatch queue */
    23 
    24   def now[A](body: => A): A =
    25   {
    26     var result: Option[A] = None
    27     if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
    28     else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
    29     result.get
    30   }
    31 
    32   def future[A](body: => A): Future[A] =
    33   {
    34     if (SwingUtilities.isEventDispatchThread()) Future.value(body)
    35     else Future.fork { now(body) }
    36   }
    37 
    38   def later(body: => Unit)
    39   {
    40     if (SwingUtilities.isEventDispatchThread()) body
    41     else SwingUtilities.invokeLater(new Runnable { def run = body })
    42   }
    43 
    44 
    45   /* delayed actions */
    46 
    47   private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
    48   {
    49     val listener = new ActionListener {
    50       override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
    51     }
    52     val timer = new Timer(time_span, listener)
    53     timer.setRepeats(false)
    54 
    55     def invoke() { if (first) timer.start() else timer.restart() }
    56     invoke _
    57   }
    58 
    59   // delayed action after first invocation
    60   def delay_first = delayed_action(true) _
    61 
    62   // delayed action after last invocation
    63   def delay_last = delayed_action(false) _
    64 }