src/Pure/System/swing_thread.scala
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 36676 ac7961d42ac3
child 38223 2a368e8e0a80
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
     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 =
    50       new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
    51     val timer = new Timer(time_span, listener)
    52     timer.setRepeats(false)
    53 
    54     def invoke() { if (first) timer.start() else timer.restart() }
    55     invoke _
    56   }
    57 
    58   // delayed action after first invocation
    59   def delay_first = delayed_action(true) _
    60 
    61   // delayed action after last invocation
    62   def delay_last = delayed_action(false) _
    63 }