improved display;
authorwenzelm
Sun, 28 Jun 2009 22:50:37 +0200
changeset 31844 3d5e51dbafe9
parent 31843 f02c6a43f1b3
child 31845 cc7ddda02436
improved display;
src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Sun Jun 28 22:35:23 2009 +0200
+++ b/src/Pure/System/gui_setup.scala	Sun Jun 28 22:50:37 2009 +0200
@@ -29,8 +29,8 @@
     // components
     val text = new TextArea {
       editable = false
-      columns = 20
-      rows = 10
+      columns = 40
+      rows = 15
       xLayoutAlignment = 0.5
     }
     val ok = new Button {
@@ -43,15 +43,15 @@
     }
 
     // values
+    if (Platform.is_windows) {
+      text.append("Cygwin root: " + Cygwin.config()._1 + "\n")
+    }
     Platform.defaults match {
       case None =>
-      case Some((name, None)) => text.append("platform: " + name + "\n")
+      case Some((name, None)) => text.append("Platform: " + name + "\n")
       case Some((name1, Some(name2))) =>
-        text.append("main platform: " + name2 + "\n")
-        text.append("alternative platform: " + name2 + "\n")
-    }
-    if (Platform.is_windows) {
-      text.append("Cygwin root: " + Cygwin.config()._1 + "\n")
+        text.append("Main platform: " + name1 + "\n")
+        text.append("Alternative platform: " + name2 + "\n")
     }
 
     // reactions