src/Pure/GUI/gui_thread.scala
changeset 67129 0262a378d5d6
parent 66094 24658c9d7c78
     1.1 --- a/src/Pure/GUI/gui_thread.scala	Mon Dec 04 18:30:28 2017 +0100
     1.2 +++ b/src/Pure/GUI/gui_thread.scala	Mon Dec 04 21:23:56 2017 +0100
     1.3 @@ -45,6 +45,16 @@
     1.4      else SwingUtilities.invokeLater(new Runnable { def run = body })
     1.5    }
     1.6  
     1.7 +  def future[A](body: => A): Future[A] =
     1.8 +  {
     1.9 +    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
    1.10 +    else {
    1.11 +      val promise = Future.promise[A]
    1.12 +      later { promise.fulfill_result(Exn.capture(body)) }
    1.13 +      promise
    1.14 +    }
    1.15 +  }
    1.16 +
    1.17  
    1.18    /* delayed events */
    1.19