# HG changeset patch
# User wenzelm
# Date 1246222237 -7200
# Node ID 3d5e51dbafe905b154e2fc132987269fc586b911
# Parent  f02c6a43f1b37cf4c5c4fd9a52de6218d1bc9c89
improved display;

diff -r f02c6a43f1b3 -r 3d5e51dbafe9 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