# HG changeset patch
# User wenzelm
# Date 1246389781 -7200
# Node ID 4a34d2a8a4970fb53563a11083e9a7aa6335ec03
# Parent  6129dea3d8a936b56ac7bcc08554d3db24191503# Parent  53acb8ec6c51e1a77ddc39c43574bea60cdb91b0
merged

diff -r 6129dea3d8a9 -r 4a34d2a8a497 src/Pure/General/swing.scala
--- a/src/Pure/General/swing.scala	Tue Jun 30 19:54:04 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-/*  Title:      Pure/General/swing.scala
-    Author:     Makarius
-
-Swing utilities.
-*/
-
-package isabelle
-
-import javax.swing.SwingUtilities
-
-object Swing
-{
-  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 later(body: => Unit) {
-    if (SwingUtilities.isEventDispatchThread) body
-    else SwingUtilities.invokeLater(new Runnable { def run = body })
-  }
-}
diff -r 6129dea3d8a9 -r 4a34d2a8a497 src/Pure/General/swing_thread.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/swing_thread.scala	Tue Jun 30 21:23:01 2009 +0200
@@ -0,0 +1,24 @@
+/*  Title:      Pure/General/swing_thread.scala
+    Author:     Makarius
+
+Evaluation within the AWT/Swing thread.
+*/
+
+package isabelle
+
+import javax.swing.SwingUtilities
+
+object Swing_Thread
+{
+  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 later(body: => Unit) {
+    if (SwingUtilities.isEventDispatchThread) body
+    else SwingUtilities.invokeLater(new Runnable { def run = body })
+  }
+}
diff -r 6129dea3d8a9 -r 4a34d2a8a497 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Jun 30 19:54:04 2009 +0200
+++ b/src/Pure/IsaMakefile	Tue Jun 30 21:23:01 2009 +0200
@@ -118,7 +118,7 @@
 ## Scala material
 
 SCALA_FILES = General/event_bus.scala General/markup.scala		\
-  General/position.scala General/scan.scala General/swing.scala		\
+  General/position.scala General/scan.scala General/swing_thread.scala	\
   General/symbol.scala General/xml.scala General/yxml.scala		\
   Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
   System/cygwin.scala System/gui_setup.scala				\
diff -r 6129dea3d8a9 -r 4a34d2a8a497 src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Tue Jun 30 19:54:04 2009 +0200
+++ b/src/Pure/System/gui_setup.scala	Tue Jun 30 21:23:01 2009 +0200
@@ -16,7 +16,7 @@
 {
   def main(args: Array[String]) =
   {
-    Swing.later {
+    Swing_Thread.later {
       UIManager.setLookAndFeel(Platform.look_and_feel)
       top.pack()
       top.visible = true