--- a/src/Pure/General/swing.scala Tue Jun 30 00:57:24 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 })
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/swing_thread.scala Tue Jun 30 21:19:32 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 })
+ }
+}
--- a/src/Pure/IsaMakefile Tue Jun 30 00:57:24 2009 +0200
+++ b/src/Pure/IsaMakefile Tue Jun 30 21:19:32 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 \
--- a/src/Pure/System/gui_setup.scala Tue Jun 30 00:57:24 2009 +0200
+++ b/src/Pure/System/gui_setup.scala Tue Jun 30 21:19:32 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