src/Pure/System/swing_thread.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 48000 880f1693299a
child 49195 9d10bd85c1be
permissions -rw-r--r--
more official command specifications, including source position;
wenzelm@36676
     1
/*  Title:      Pure/System/swing_thread.scala
wenzelm@45673
     2
    Module:     PIDE
wenzelm@29202
     3
    Author:     Makarius
wenzelm@31942
     4
    Author:     Fabian Immler, TU Munich
wenzelm@29202
     5
wenzelm@31862
     6
Evaluation within the AWT/Swing thread.
wenzelm@29202
     7
*/
wenzelm@29202
     8
wenzelm@29202
     9
package isabelle
wenzelm@29202
    10
wenzelm@31942
    11
import javax.swing.{SwingUtilities, Timer}
wenzelm@31942
    12
import java.awt.event.{ActionListener, ActionEvent}
wenzelm@31942
    13
wenzelm@29202
    14
wenzelm@31862
    15
object Swing_Thread
wenzelm@29202
    16
{
wenzelm@32494
    17
  /* checks */
wenzelm@32494
    18
wenzelm@32494
    19
  def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
wenzelm@32494
    20
  def require() = Predef.require(SwingUtilities.isEventDispatchThread())
wenzelm@32494
    21
wenzelm@32494
    22
wenzelm@31942
    23
  /* main dispatch queue */
wenzelm@31942
    24
wenzelm@34026
    25
  def now[A](body: => A): A =
wenzelm@34026
    26
  {
wenzelm@48000
    27
    if (SwingUtilities.isEventDispatchThread()) body
wenzelm@48000
    28
    else {
wenzelm@48000
    29
      lazy val result = { assert(); Exn.capture(body) }
wenzelm@48000
    30
      SwingUtilities.invokeAndWait(new Runnable { def run = result })
wenzelm@48000
    31
      Exn.release(result)
wenzelm@48000
    32
    }
wenzelm@29649
    33
  }
wenzelm@29202
    34
wenzelm@34299
    35
  def future[A](body: => A): Future[A] =
wenzelm@34299
    36
  {
wenzelm@34299
    37
    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
wenzelm@34299
    38
    else Future.fork { now(body) }
wenzelm@34299
    39
  }
wenzelm@34026
    40
wenzelm@34299
    41
  def later(body: => Unit)
wenzelm@34299
    42
  {
wenzelm@32494
    43
    if (SwingUtilities.isEventDispatchThread()) body
wenzelm@29649
    44
    else SwingUtilities.invokeLater(new Runnable { def run = body })
wenzelm@29649
    45
  }
wenzelm@31942
    46
wenzelm@31942
    47
wenzelm@31942
    48
  /* delayed actions */
wenzelm@31942
    49
wenzelm@46740
    50
  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Boolean => Unit =
wenzelm@31942
    51
  {
wenzelm@38223
    52
    val listener = new ActionListener {
wenzelm@38223
    53
      override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
wenzelm@38223
    54
    }
wenzelm@40848
    55
    val timer = new Timer(time.ms.toInt, listener)
wenzelm@32501
    56
    timer.setRepeats(false)
wenzelm@32501
    57
wenzelm@46574
    58
    def invoke() { later { if (first) timer.start() else timer.restart() } }
wenzelm@46740
    59
    def revoke() { timer.stop() }
wenzelm@46740
    60
wenzelm@46740
    61
    (active: Boolean) => if (active) invoke() else revoke()
wenzelm@31942
    62
  }
wenzelm@32501
    63
wenzelm@32501
    64
  // delayed action after first invocation
wenzelm@32501
    65
  def delay_first = delayed_action(true) _
wenzelm@32501
    66
wenzelm@32501
    67
  // delayed action after last invocation
wenzelm@32501
    68
  def delay_last = delayed_action(false) _
wenzelm@29202
    69
}