equal
deleted
inserted
replaced
8 package isabelle |
8 package isabelle |
9 |
9 |
10 import javax.swing.{SwingUtilities, Timer} |
10 import javax.swing.{SwingUtilities, Timer} |
11 import java.awt.event.{ActionListener, ActionEvent} |
11 import java.awt.event.{ActionListener, ActionEvent} |
12 |
12 |
|
13 import scala.actors.{Future, Futures} |
|
14 |
13 |
15 |
14 object Swing_Thread |
16 object Swing_Thread |
15 { |
17 { |
16 /* checks */ |
18 /* checks */ |
17 |
19 |
19 def require() = Predef.require(SwingUtilities.isEventDispatchThread()) |
21 def require() = Predef.require(SwingUtilities.isEventDispatchThread()) |
20 |
22 |
21 |
23 |
22 /* main dispatch queue */ |
24 /* main dispatch queue */ |
23 |
25 |
24 def now[A](body: => A): A = { |
26 def now[A](body: => A): A = |
|
27 { |
25 var result: Option[A] = None |
28 var result: Option[A] = None |
26 if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } |
29 if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } |
27 else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) |
30 else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) |
28 result.get |
31 result.get |
29 } |
32 } |
|
33 |
|
34 def future[A](body: => A): Future[A] = |
|
35 Futures.future(now(body)) |
30 |
36 |
31 def later(body: => Unit) { |
37 def later(body: => Unit) { |
32 if (SwingUtilities.isEventDispatchThread()) body |
38 if (SwingUtilities.isEventDispatchThread()) body |
33 else SwingUtilities.invokeLater(new Runnable { def run = body }) |
39 else SwingUtilities.invokeLater(new Runnable { def run = body }) |
34 } |
40 } |