src/Pure/System/swing_thread.scala
author wenzelm
Mon Aug 23 16:53:22 2010 +0200 (2010-08-23)
changeset 38639 f642faca303e
parent 38223 2a368e8e0a80
child 38847 57043221eb43
permissions -rw-r--r--
main session actor as independent thread, to avoid starvation via regular worker pool;
tuned;
     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 }