author | wenzelm |
Sat, 29 Jun 2013 12:57:04 +0200 | |
changeset 52477 | 025b3777e592 |
parent 49251 | cd28155bb7d5 |
child 52859 | f31624cc4467 |
permissions | -rw-r--r-- |
36676 | 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 | 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 | 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 | 7 |
*/ |
8 |
||
9 |
package isabelle |
|
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 | 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 | 16 |
{ |
32494 | 17 |
/* checks */ |
18 |
||
19 |
def assert() = Predef.assert(SwingUtilities.isEventDispatchThread()) |
|
20 |
def require() = Predef.require(SwingUtilities.isEventDispatchThread()) |
|
21 |
||
52477 | 22 |
def required[A](body: => A): A = { require(); body } |
23 |
||
32494 | 24 |
|
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
25 |
/* main dispatch queue */ |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
26 |
|
34026 | 27 |
def now[A](body: => A): A = |
28 |
{ |
|
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
|
29 |
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
|
30 |
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
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
} |
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
35 |
} |
29202 | 36 |
|
34299
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
37 |
def future[A](body: => A): Future[A] = |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
38 |
{ |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
39 |
if (SwingUtilities.isEventDispatchThread()) Future.value(body) |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
40 |
else Future.fork { now(body) } |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
41 |
} |
34026 | 42 |
|
34299
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
43 |
def later(body: => Unit) |
68716caa7745
Swing_Thread.future: plain Future.value if this is already Swing;
wenzelm
parents:
34217
diff
changeset
|
44 |
{ |
32494 | 45 |
if (SwingUtilities.isEventDispatchThread()) body |
29649
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
46 |
else SwingUtilities.invokeLater(new Runnable { def run = body }) |
8b0c1397868e
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm
parents:
29202
diff
changeset
|
47 |
} |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
48 |
|
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
49 |
|
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
50 |
/* delayed actions */ |
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
51 |
|
49195 | 52 |
abstract class Delay extends |
31942
63466160ff27
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
wenzelm
parents:
31862
diff
changeset
|
53 |
{ |
49195 | 54 |
def invoke(): Unit |
55 |
def revoke(): Unit |
|
49196
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
56 |
def postpone(time: Time): Unit |
49195 | 57 |
} |
58 |
||
49249 | 59 |
private def delayed_action(first: Boolean)(time: => Time)(action: => Unit): Delay = |
49195 | 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() |
|
49249 | 66 |
timer.setInitialDelay(time.ms.toInt) |
49195 | 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() |
|
49249 | 81 |
timer.setInitialDelay(time.ms.toInt) |
49195 | 82 |
} |
49196
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
83 |
|
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
84 |
def postpone(alt_time: Time) |
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
85 |
{ |
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
86 |
require() |
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
87 |
if (timer.isRunning) { |
49251 | 88 |
timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt) |
49196
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
89 |
timer.restart() |
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
90 |
} |
1d63ceb0d177
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents:
49195
diff
changeset
|
91 |
} |
38223 | 92 |
} |
32501 | 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) _ |
|
29202 | 99 |
} |