src/Pure/System/swing_thread.scala
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48000 880f1693299a
child 49195 9d10bd85c1be
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 34299
diff changeset
     1
/*  Title:      Pure/System/swing_thread.scala
45673
cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents: 45667
diff changeset
     2
    Module:     PIDE
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
     4
    Author:     Fabian Immler, TU Munich
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     5
31862
53acb8ec6c51 renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents: 29777
diff changeset
     6
Evaluation within the AWT/Swing thread.
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     7
*/
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     8
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
     9
package isabelle
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    10
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    11
import javax.swing.{SwingUtilities, Timer}
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    12
import java.awt.event.{ActionListener, ActionEvent}
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    13
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    14
31862
53acb8ec6c51 renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
wenzelm
parents: 29777
diff changeset
    15
object Swing_Thread
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    16
{
32494
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    17
  /* checks */
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    18
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    19
  def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    20
  def require() = Predef.require(SwingUtilities.isEventDispatchThread())
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    21
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    22
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    23
  /* main dispatch queue */
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    24
34026
0cb44ac299f8 added future;
wenzelm
parents: 32501
diff changeset
    25
  def now[A](body: => A): A =
0cb44ac299f8 added future;
wenzelm
parents: 32501
diff changeset
    26
  {
48000
880f1693299a further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents: 47989
diff changeset
    27
    if (SwingUtilities.isEventDispatchThread()) body
880f1693299a further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents: 47989
diff changeset
    28
    else {
880f1693299a further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents: 47989
diff changeset
    29
      lazy val result = { assert(); Exn.capture(body) }
880f1693299a further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents: 47989
diff changeset
    30
      SwingUtilities.invokeAndWait(new Runnable { def run = result })
880f1693299a further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents: 47989
diff changeset
    31
      Exn.release(result)
880f1693299a further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;
wenzelm
parents: 47989
diff changeset
    32
    }
29649
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    33
  }
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    34
34299
68716caa7745 Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents: 34217
diff changeset
    35
  def future[A](body: => A): Future[A] =
68716caa7745 Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents: 34217
diff changeset
    36
  {
68716caa7745 Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents: 34217
diff changeset
    37
    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
68716caa7745 Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents: 34217
diff changeset
    38
    else Future.fork { now(body) }
68716caa7745 Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents: 34217
diff changeset
    39
  }
34026
0cb44ac299f8 added future;
wenzelm
parents: 32501
diff changeset
    40
34299
68716caa7745 Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents: 34217
diff changeset
    41
  def later(body: => Unit)
68716caa7745 Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents: 34217
diff changeset
    42
  {
32494
4ab2292e452a explicit checks;
wenzelm
parents: 31942
diff changeset
    43
    if (SwingUtilities.isEventDispatchThread()) body
29649
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    44
    else SwingUtilities.invokeLater(new Runnable { def run = body })
8b0c1397868e more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents: 29202
diff changeset
    45
  }
31942
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
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    48
  /* delayed actions */
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    49
46740
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46574
diff changeset
    50
  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Boolean => Unit =
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    51
  {
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 36676
diff changeset
    52
    val listener = new ActionListener {
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 36676
diff changeset
    53
      override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 36676
diff changeset
    54
    }
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 38847
diff changeset
    55
    val timer = new Timer(time.ms.toInt, listener)
32501
41aa620885c2 refined delay into delay_first/delay_last;
wenzelm
parents: 32494
diff changeset
    56
    timer.setRepeats(false)
41aa620885c2 refined delay into delay_first/delay_last;
wenzelm
parents: 32494
diff changeset
    57
46574
41701fce8ac7 invoke later to reduce chance of causing deadlock;
wenzelm
parents: 45673
diff changeset
    58
    def invoke() { later { if (first) timer.start() else timer.restart() } }
46740
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46574
diff changeset
    59
    def revoke() { timer.stop() }
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46574
diff changeset
    60
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46574
diff changeset
    61
    (active: Boolean) => if (active) invoke() else revoke()
31942
63466160ff27 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents: 31862
diff changeset
    62
  }
32501
41aa620885c2 refined delay into delay_first/delay_last;
wenzelm
parents: 32494
diff changeset
    63
41aa620885c2 refined delay into delay_first/delay_last;
wenzelm
parents: 32494
diff changeset
    64
  // delayed action after first invocation
41aa620885c2 refined delay into delay_first/delay_last;
wenzelm
parents: 32494
diff changeset
    65
  def delay_first = delayed_action(true) _
41aa620885c2 refined delay into delay_first/delay_last;
wenzelm
parents: 32494
diff changeset
    66
41aa620885c2 refined delay into delay_first/delay_last;
wenzelm
parents: 32494
diff changeset
    67
  // delayed action after last invocation
41aa620885c2 refined delay into delay_first/delay_last;
wenzelm
parents: 32494
diff changeset
    68
  def delay_last = delayed_action(false) _
29202
2454172eddae Swing utilities.
wenzelm
parents:
diff changeset
    69
}