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