simplified alignment via FlowPanel;
authorwenzelm
Thu, 20 May 2010 15:51:28 +0200
changeset 36994 797af3ebd5f1
parent 36993 b7cce32953f0
child 36995 9421452afc29
simplified alignment via FlowPanel; tuned;
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)