1/*  Title:      Pure/GUI/gui_thread.scala
2    Author:     Makarius
3
4Evaluation within the GUI thread (for AWT/Swing).
5*/
6
7package isabelle
8
9
10import javax.swing.SwingUtilities
11
12
13object GUI_Thread
14{
15  /* context check */
16
17  def assert[A](body: => A): A =
18  {
19    Predef.assert(SwingUtilities.isEventDispatchThread())
20    body
21  }
22
23  def require[A](body: => A): A =
24  {
25    Predef.require(SwingUtilities.isEventDispatchThread())
26    body
27  }
28
29
30  /* event dispatch queue */
31
32  def now[A](body: => A): A =
33  {
34    if (SwingUtilities.isEventDispatchThread()) body
35    else {
36      lazy val result = { assert { Exn.capture(body) } }
37      SwingUtilities.invokeAndWait(new Runnable { def run = result })
38      Exn.release(result)
39    }
40  }
41
42  def later(body: => Unit)
43  {
44    if (SwingUtilities.isEventDispatchThread()) body
45    else SwingUtilities.invokeLater(new Runnable { def run = body })
46  }
47
48  def future[A](body: => A): Future[A] =
49  {
50    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
51    else {
52      val promise = Future.promise[A]
53      later { promise.fulfill_result(Exn.capture(body)) }
54      promise
55    }
56  }
57
58
59  /* delayed events */
60
61  def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
62    Standard_Thread.delay_first(delay) { later { event } }
63
64  def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
65    Standard_Thread.delay_last(delay) { later { event } }
66}
67