changeset 67129 | 0262a378d5d6 |
parent 66094 | 24658c9d7c78 |
child 71692 | f8e52c0152fe |
--- a/src/Pure/GUI/gui_thread.scala Mon Dec 04 18:30:28 2017 +0100 +++ b/src/Pure/GUI/gui_thread.scala Mon Dec 04 21:23:56 2017 +0100 @@ -45,6 +45,16 @@ else SwingUtilities.invokeLater(new Runnable { def run = body }) } + def future[A](body: => A): Future[A] = + { + if (SwingUtilities.isEventDispatchThread()) Future.value(body) + else { + val promise = Future.promise[A] + later { promise.fulfill_result(Exn.capture(body)) } + promise + } + } + /* delayed events */