# HG changeset patch
# User wenzelm
# Date 1271533229 -7200
# Node ID 9c098598db2a4c41f5e60fbbf9bd3db2c8cbee4a
# Parent  8e61560ded89a682c8aaa25fc036bccca0dc0613
system properties determine the JVM platform, not the Isabelle one;

diff -r 8e61560ded89 -r 9c098598db2a src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Sat Apr 17 21:01:55 2010 +0200
+++ b/src/Pure/System/gui_setup.scala	Sat Apr 17 21:40:29 2010 +0200
@@ -43,16 +43,9 @@
     }
 
     // values
-    Platform.defaults match {
-      case None =>
-      case Some((name, None)) => text.append("Platform: " + name + "\n")
-      case Some((name1, Some(name2))) =>
-        text.append("Main platform: " + name1 + "\n")
-        text.append("Alternative platform: " + name2 + "\n")
-    }
-    if (Platform.is_windows) {
+    text.append("JVM platform: " + Platform.jvm_platform() + "\n")
+    if (Platform.is_windows)
       text.append("Cygwin root: " + Cygwin.check_root() + "\n")
-    }
     try {
       val isabelle_system = new Isabelle_System
       text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
diff -r 8e61560ded89 -r 9c098598db2a src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Sat Apr 17 21:01:55 2010 +0200
+++ b/src/Pure/System/platform.scala	Sat Apr 17 21:40:29 2010 +0200
@@ -19,37 +19,37 @@
   val is_windows = System.getProperty("os.name").startsWith("Windows")
 
 
-  /* Isabelle platform identifiers */
+  /* Platform identifiers */
 
   private val Solaris = new Regex("SunOS|Solaris")
   private val Linux = new Regex("Linux")
   private val Darwin = new Regex("Mac OS X")
-  private val Cygwin = new Regex("Windows.*")
+  private val Windows = new Regex("Windows.*")
 
   private val X86 = new Regex("i.86|x86")
   private val X86_64 = new Regex("amd64|x86_64")
   private val Sparc = new Regex("sparc")
   private val PPC = new Regex("PowerPC|ppc")
 
-  // main default, optional 64bit variant
-  val defaults: Option[(String, Option[String])] =
+  def jvm_platform(): String =
   {
-    (java.lang.System.getProperty("os.name") match {
-      case Solaris() => Some("solaris")
-      case Linux() => Some("linux")
-      case Darwin() => Some("darwin")
-      case Cygwin() => Some("cygwin")
-      case _ => None
-    }) match {
-      case Some(name) =>
-        java.lang.System.getProperty("os.arch") match {
-          case X86() => Some(("x86-" + name, None))
-          case X86_64() => Some(("x86-" + name, if (is_windows) None else Some("x86_64-" + name)))
-          case Sparc() => Some(("sparc-" + name, None))
-          case PPC() => Some(("ppc-" + name, None))
-        }
-      case None => None
-    }
+    val arch =
+      java.lang.System.getProperty("os.arch") match {
+        case X86() => "x86"
+        case X86_64() => "x86_64"
+        case Sparc() => "sparc"
+        case PPC() => "ppc"
+        case _ => error("Failed to determine CPU architecture")
+      }
+    val os =
+      java.lang.System.getProperty("os.name") match {
+        case Solaris() => "solaris"
+        case Linux() => "linux"
+        case Darwin() => "darwin"
+        case Windows() => "windows"
+        case _ => error("Failed to determine operating system platform")
+      }
+    arch + "-" + os
   }