# HG changeset patch
# User wenzelm
# Date 1512419036 -3600
# Node ID 0262a378d5d6e223c903144eb148b0e88cf05f0c
# Parent  4d91b6d5d49cad83f756c06302a2f1f11b5479b1
added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;

diff -r 4d91b6d5d49c -r 0262a378d5d6 src/Pure/GUI/gui_thread.scala
--- 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 */