# HG changeset patch
# User wenzelm
# Date 1233139005 -3600
# Node ID 8b0c1397868e7b46bc8d6066654e5562be216347
# Parent  ead544f3d6a11026931a0ae74a5ecb563485d229
more robust treatment of SwingUtilities.isEventDispatchThread;

diff -r ead544f3d6a1 -r 8b0c1397868e src/Pure/General/swing.scala
--- a/src/Pure/General/swing.scala	Wed Jan 28 10:43:31 2009 +0100
+++ b/src/Pure/General/swing.scala	Wed Jan 28 11:36:45 2009 +0100
@@ -10,9 +10,13 @@
 
 object Swing
 {
-  def now(body: => Unit) =
-    SwingUtilities.invokeAndWait(new Runnable { def run = body })
+  def now(body: => Unit) {
+    if (SwingUtilities.isEventDispatchThread) body
+    else SwingUtilities.invokeAndWait(new Runnable { def run = body })
+  }
 
-  def later(body: => Unit) =
-    SwingUtilities.invokeLater(new Runnable { def run = body })
+  def later(body: => Unit) {
+    if (SwingUtilities.isEventDispatchThread) body
+    else SwingUtilities.invokeLater(new Runnable { def run = body })
+  }
 }