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