simplified alignment via FlowPanel;
authorwenzelm
Thu, 20 May 2010 15:51:28 +0200
changeset 37009797af3ebd5f1
parent 37008 b7cce32953f0
child 37010 9421452afc29
simplified alignment via FlowPanel;
tuned;
src/Pure/System/gui_setup.scala
     1.1 --- a/src/Pure/System/gui_setup.scala	Thu May 20 13:54:31 2010 +0200
     1.2 +++ b/src/Pure/System/gui_setup.scala	Thu May 20 15:51:28 2010 +0200
     1.3 @@ -6,8 +6,8 @@
     1.4  
     1.5  package isabelle
     1.6  
     1.7 -import scala.swing._
     1.8 -import scala.swing.event._
     1.9 +import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication}
    1.10 +import scala.swing.event.ButtonClicked
    1.11  
    1.12  
    1.13  object GUI_Setup extends SwingApplication
    1.14 @@ -27,16 +27,14 @@
    1.15        editable = false
    1.16        columns = 80
    1.17        rows = 20
    1.18 -      xLayoutAlignment = 0.5
    1.19      }
    1.20 -    val ok = new Button {
    1.21 -      text = "OK"
    1.22 -      xLayoutAlignment = 0.5
    1.23 -    }
    1.24 -    contents = new BoxPanel(Orientation.Vertical) {
    1.25 -      contents += text
    1.26 -      contents += ok
    1.27 -    }
    1.28 +    val ok = new Button { text = "OK" }
    1.29 +    val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
    1.30 +
    1.31 +    val panel = new BorderPanel
    1.32 +    panel.layout(text) = BorderPanel.Position.Center
    1.33 +    panel.layout(ok_panel) = BorderPanel.Position.South
    1.34 +    contents = panel
    1.35  
    1.36      // values
    1.37      if (Platform.is_windows)