src/Pure/General/swing_thread.scala
author wenzelm
Wed, 02 Sep 2009 20:49:04 +0200
changeset 32494 4ab2292e452a
parent 31942 63466160ff27
child 32501 41aa620885c2
permissions -rw-r--r--
explicit checks;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31862
53acb8ec6c51 renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents: 29777
diff changeset
     1
/*  Title:      Pure/General/swing_thread.scala
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
     3
    Author:     Fabian Immler, TU Munich
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     4
31862
53acb8ec6c51 renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents: 29777
diff changeset
     5
Evaluation within the AWT/Swing thread.
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     6
*/
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     7
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     8
package isabelle
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     9
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    10
import javax.swing.{SwingUtilities, Timer}
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    11
import java.awt.event.{ActionListener, ActionEvent}
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    12
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    13
31862
53acb8ec6c51 renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents: 29777
diff changeset
    14
object Swing_Thread
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    15
{
32494
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    16
  /* checks */
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    17
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    18
  def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    19
  def require() = Predef.require(SwingUtilities.isEventDispatchThread())
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    20
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    21
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    22
  /* main dispatch queue */
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    23
29777
f3284860004c result for Swing.now;
wenzelm
parents: 29649
diff changeset
    24
  def now[A](body: => A): A = {
f3284860004c result for Swing.now;
wenzelm
parents: 29649
diff changeset
    25
    var result: Option[A] = None
32494
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    26
    if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
29777
f3284860004c result for Swing.now;
wenzelm
parents: 29649
diff changeset
    27
    else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
f3284860004c result for Swing.now;
wenzelm
parents: 29649
diff changeset
    28
    result.get
29649
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    29
  }
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    30
29649
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    31
  def later(body: => Unit) {
32494
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    32
    if (SwingUtilities.isEventDispatchThread()) body
29649
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    33
    else SwingUtilities.invokeLater(new Runnable { def run = body })
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    34
  }
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    35
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    36
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    37
  /* delayed actions */
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    38
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    39
  // turn multiple invocations into single action within time span
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    40
  def delay(time_span: Int)(action: => Unit): () => Unit =
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    41
  {
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    42
    val listener =
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    43
      new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    44
    val timer = new Timer(time_span, listener)
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    45
    def invoke()
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    46
    {
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    47
      if (!timer.isRunning()) {
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    48
        timer.setRepeats(false)
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    49
        timer.start()
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    50
      }
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    51
    }
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    52
    invoke _
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    53
  }
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    54
}