# HG changeset patch
# User wenzelm
# Date 1260272507 -3600
# Node ID 0cb44ac299f810d7d3720b632d979ccd4f7b28a3
# Parent  7996b488a9b509a3019531a9f71076a28e91c78b
added future;

diff -r 7996b488a9b5 -r 0cb44ac299f8 src/Pure/General/swing_thread.scala
--- a/src/Pure/General/swing_thread.scala	Mon Dec 07 23:06:03 2009 +0100
+++ b/src/Pure/General/swing_thread.scala	Tue Dec 08 12:41:47 2009 +0100
@@ -10,6 +10,8 @@
 import javax.swing.{SwingUtilities, Timer}
 import java.awt.event.{ActionListener, ActionEvent}
 
+import scala.actors.{Future, Futures}
+
 
 object Swing_Thread
 {
@@ -21,13 +23,17 @@
 
   /* main dispatch queue */
 
-  def now[A](body: => A): A = {
+  def now[A](body: => A): A =
+  {
     var result: Option[A] = None
     if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
     else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
     result.get
   }
 
+  def future[A](body: => A): Future[A] =
+    Futures.future(now(body))
+
   def later(body: => Unit) {
     if (SwingUtilities.isEventDispatchThread()) body
     else SwingUtilities.invokeLater(new Runnable { def run = body })