src/Pure/System/swing_thread.scala
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 52477 025b3777e592
child 52859 f31624cc4467
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
     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   def required[A](body: => A): A = { require(); body }
    23 
    24 
    25   /* main dispatch queue */
    26 
    27   def now[A](body: => A): A =
    28   {
    29     if (SwingUtilities.isEventDispatchThread()) body
    30     else {
    31       lazy val result = { assert(); Exn.capture(body) }
    32       SwingUtilities.invokeAndWait(new Runnable { def run = result })
    33       Exn.release(result)
    34     }
    35   }
    36 
    37   def future[A](body: => A): Future[A] =
    38   {
    39     if (SwingUtilities.isEventDispatchThread()) Future.value(body)
    40     else Future.fork { now(body) }
    41   }
    42 
    43   def later(body: => Unit)
    44   {
    45     if (SwingUtilities.isEventDispatchThread()) body
    46     else SwingUtilities.invokeLater(new Runnable { def run = body })
    47   }
    48 
    49 
    50   /* delayed actions */
    51 
    52   abstract class Delay extends
    53   {
    54     def invoke(): Unit
    55     def revoke(): Unit
    56     def postpone(time: Time): Unit
    57   }
    58 
    59   private def delayed_action(first: Boolean)(time: => Time)(action: => Unit): Delay =
    60     new Delay {
    61       private val timer = new Timer(time.ms.toInt, null)
    62       timer.setRepeats(false)
    63       timer.addActionListener(new ActionListener {
    64         override def actionPerformed(e: ActionEvent) {
    65           assert()
    66           timer.setInitialDelay(time.ms.toInt)
    67           action
    68         }
    69       })
    70 
    71       def invoke()
    72       {
    73         require()
    74         if (first) timer.start() else timer.restart()
    75       }
    76 
    77       def revoke()
    78       {
    79         require()
    80         timer.stop()
    81         timer.setInitialDelay(time.ms.toInt)
    82       }
    83 
    84       def postpone(alt_time: Time)
    85       {
    86         require()
    87         if (timer.isRunning) {
    88           timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
    89           timer.restart()
    90         }
    91       }
    92     }
    93 
    94   // delayed action after first invocation
    95   def delay_first = delayed_action(true) _
    96 
    97   // delayed action after last invocation
    98   def delay_last = delayed_action(false) _
    99 }