moved platform identification to platform.scala;
more precise discrimination, including 64bit option;

--- a/src/Pure/IsaMakefile	Sat Jun 27 22:28:07 2009 +0200
+++ b/src/Pure/IsaMakefile	Sun Jun 28 14:27:42 2009 +0200
@@ -122,8 +122,9 @@
   General/symbol.scala General/xml.scala General/yxml.scala		\
   Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
   System/cygwin.scala System/isabelle_process.scala			\
-  System/isabelle_system.scala Thy/completion.scala			\
-  Thy/thy_header.scala Tools/isabelle_syntax.scala
+  System/isabelle_system.scala System/platform.scala			\
+  Thy/completion.scala Thy/thy_header.scala				\
+  Tools/isabelle_syntax.scala
 
 
 SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar

--- a/src/Pure/System/isabelle_system.scala	Sat Jun 27 22:28:07 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Jun 28 14:27:42 2009 +0200
@@ -19,42 +19,6 @@
   val charset = "UTF-8"
 
 
-  /* platform identification */
-
-  val is_cygwin = System.getProperty("os.name").startsWith("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")
-
-  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.*")
-
-  val default_platform: Option[String] =
-  {
-    val name =
-      java.lang.System.getProperty("os.name") match {
-        case Solaris() => "solaris"
-        case Linux() => "linux"
-        case Darwin() => "darwin"
-        case Cygwin() => "cygwin"
-        case _ => ""
-      }
-    val arch =
-      java.lang.System.getProperty("os.arch") match {
-        case X86() | X86_64() => "x86"
-        case Sparc() => "sparc"
-        case PPC() => "ppc"
-        case _ => ""
-      }
-    if (arch == "" || name == "") None
-    else Some(arch + "-" + name)
-  }
-
-
   /* shell processes */
 
   private def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process =
@@ -98,7 +62,7 @@
 
   private val (platform_root, drive_prefix, shell_prefix) =
   {
-    if (Isabelle_System.is_cygwin) {
+    if (Platform.is_windows) {
       val root = Cygwin.root() getOrElse "C:\\cygwin"
       val drive = Cygwin.cygdrive() getOrElse "/cygdrive"
       val shell = List(root + "\\bin\\bash", "-l")
@@ -220,7 +184,7 @@
     val result_path = new StringBuilder
     val rest =
       expand_path(isabelle_path) match {
-        case Cygdrive(drive, rest) if Isabelle_System.is_cygwin =>
+        case Cygdrive(drive, rest) if Platform.is_windows =>
           result_path ++= (drive + ":" + File.separator)
           rest
         case path if path.startsWith("/") =>
@@ -248,7 +212,7 @@
 
   def isabelle_path(platform_path: String): String =
   {
-    if (Isabelle_System.is_cygwin) {
+    if (Platform.is_windows) {
       platform_path.replace('/', '\\') match {
         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
         case Drive(letter, rest) =>
@@ -286,7 +250,7 @@
   def execute(redirect: Boolean, args: String*): Process =
   {
     val cmdline =
-      if (Isabelle_System.is_cygwin) List(platform_path("/bin/env")) ++ args
+      if (Platform.is_windows) List(platform_path("/bin/env")) ++ args
       else args
     Isabelle_System.raw_execute(environment, redirect, cmdline: _*)
   }
@@ -325,7 +289,7 @@
   {
     // blocks until writer is ready
     val stream =
-      if (Isabelle_System.is_cygwin) execute(false, "cat", fifo).getInputStream
+      if (Platform.is_windows) execute(false, "cat", fifo).getInputStream
       else new FileInputStream(fifo)
     new BufferedReader(new InputStreamReader(stream, Isabelle_System.charset))
   }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/platform.scala	Sun Jun 28 14:27:42 2009 +0200
@@ -0,0 +1,48 @@
+/*  Title:      Pure/System/platform.scala
+    Author:     Makarius
+
+Raw platform identification.
+*/
+
+package isabelle
+
+import scala.util.matching.Regex
+
+
+object Platform
+{
+  val is_macos = System.getProperty("os.name") == "Mac OS X"
+  val is_windows = System.getProperty("os.name").startsWith("Windows")
+
+  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 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])] =
+  {
+    (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
+    }
+  }
+}
+