--- a/src/Pure/System/gui_setup.scala Wed May 05 23:09:34 2010 +0200
+++ b/src/Pure/System/gui_setup.scala Wed May 05 23:22:11 2010 +0200
@@ -12,15 +12,13 @@
import scala.swing.event._
-object GUI_Setup extends GUIApplication
+object GUI_Setup extends SwingApplication
{
- def main(args: Array[String]) =
+ def startup(args: Array[String]) =
{
- Swing_Thread.later {
- UIManager.setLookAndFeel(Platform.look_and_feel)
- top.pack()
- top.visible = true
- }
+ UIManager.setLookAndFeel(Platform.look_and_feel)
+ top.pack()
+ top.visible = true
}
def top = new MainFrame {