# HG changeset patch
# User wenzelm
# Date 1274363488 -7200
# Node ID 797af3ebd5f1446e237d20edaf5bb0b1814b2e90
# Parent  b7cce32953f016ca37bbf2e80b98d6c8d1c9f6b9
simplified alignment via FlowPanel;
tuned;

diff -r b7cce32953f0 -r 797af3ebd5f1 src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Thu May 20 13:54:31 2010 +0200
+++ b/src/Pure/System/gui_setup.scala	Thu May 20 15:51:28 2010 +0200
@@ -6,8 +6,8 @@
 
 package isabelle
 
-import scala.swing._
-import scala.swing.event._
+import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication}
+import scala.swing.event.ButtonClicked
 
 
 object GUI_Setup extends SwingApplication
@@ -27,16 +27,14 @@
       editable = false
       columns = 80
       rows = 20
-      xLayoutAlignment = 0.5
     }
-    val ok = new Button {
-      text = "OK"
-      xLayoutAlignment = 0.5
-    }
-    contents = new BoxPanel(Orientation.Vertical) {
-      contents += text
-      contents += ok
-    }
+    val ok = new Button { text = "OK" }
+    val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
+
+    val panel = new BorderPanel
+    panel.layout(text) = BorderPanel.Position.Center
+    panel.layout(ok_panel) = BorderPanel.Position.South
+    contents = panel
 
     // values
     if (Platform.is_windows)