# HG changeset patch
# User wenzelm
# Date 1478874296 -3600
# Node ID a2eebcc8bb696c9752a8c13e7c1b1083f43153ce
# Parent  98215fa4f8d1cefb4ca60c229d4862be8c199b22
clarified platform selection;

diff -r 98215fa4f8d1 -r a2eebcc8bb69 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Fri Nov 11 13:57:01 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Fri Nov 11 15:24:56 2016 +0100
@@ -52,38 +52,34 @@
             "/mingw64/bin/libgmp-10.dll",
             "/mingw64/bin/libstdc++-6.dll")))
 
-  lazy val default_platform =
-    Isabelle_System.getenv_strict("ISABELLE_PLATFORM32") match {
-      case "x86-cygwin" => "x86-windows"
-      case platform => platform
-    }
-
   def build_polyml(
     root: Path,
     progress: Progress = Ignore_Progress,
-    platform: String = default_platform,
+    arch_64: Boolean = false,
     options: List[String] = Nil,
     other_bash: String = "")
   {
     if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
       error("Bad Poly/ML root directory: " + root)
 
+    val platform =
+      (if (arch_64) "x86_64" else "x86") +
+      (if (Platform.is_windows) "-windows" else if (Platform.is_macos) "-darwin" else "-linux")
+
     val info =
       platform_info.get(platform) getOrElse
         error("Bad platform identifier: " + quote(platform))
 
-    if (platform.endsWith("windows") && other_bash == "")
+    if (Platform.is_windows && other_bash == "")
       error("Windows requires other bash (for msys)")
 
 
     /* configure and make */
 
-    val multilib =
-      platform == "x86-linux" && Isabelle_System.getenv("ISABELLE_PLATFORM64") == "x86_64-linux"
-
     val configure_options =
-      (if (multilib) info.options_multilib else info.options) :::
-        List("--enable-intinf-as-int") ::: options
+      (if (!arch_64 && Isabelle_System.getenv("ISABELLE_PLATFORM64") == "x86_64-linux")
+        info.options_multilib
+       else info.options) ::: List("--enable-intinf-as-int") ::: options
 
     val script =
       info.setup + "\n" +
@@ -103,7 +99,7 @@
       progress_stderr = progress.echo(_)).check
 
     val lib_files =
-      if (platform.endsWith("linux")) {
+      if (Platform.is_linux) {
         val libs = Isabelle_System.bash("ldd target/bin/poly", cwd = root.file).check.out_lines
         val Pattern = """\s*libgmp.*=>\s*(\S+).*""".r
         for (Pattern(lib) <- libs) yield lib
@@ -134,20 +130,25 @@
   {
     Command_Line.tool0 {
       var other_bash = ""
-      var platform = default_platform
+      var arch_64 = false
 
       val getopts = Getopts("""
 Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
 
   Options are:
     -b EXE       other bash executable (notably for msys on Windows)
-    -p PLATFORM  platform identifier and target directory (default: """ + default_platform + """)
+    -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
 
   Build Poly/ML in its source ROOT directory of its sources, with additional
   CONFIGURE_OPTIONS (e.g. --with-gmp).
 """,
         "b:" -> (arg => other_bash = arg),
-        "p:" -> (arg => platform = arg))
+        "m:" ->
+          {
+            case "32" | "x86" => arch_64 = false
+            case "64" | "x86_64" => arch_64 = true
+            case bad => error("Bad processor architecture: " + quote(bad))
+          })
 
       val more_args = getopts(args)
       val (root, options) =
@@ -155,7 +156,7 @@
           case root :: options => (Path.explode(root), options)
           case Nil => getopts.usage()
         }
-      build_polyml(root, progress = new Console_Progress, platform = platform, options = options,
+      build_polyml(root, progress = new Console_Progress, arch_64 = arch_64, options = options,
           other_bash = other_bash)
     }
   }
diff -r 98215fa4f8d1 -r a2eebcc8bb69 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Fri Nov 11 13:57:01 2016 +0100
+++ b/src/Pure/System/platform.scala	Fri Nov 11 15:24:56 2016 +0100
@@ -14,6 +14,7 @@
 {
   /* main OS variants */
 
+  val is_linux = System.getProperty("os.name", "") == "Linux"
   val is_macos = System.getProperty("os.name", "") == "Mac OS X"
   val is_windows = System.getProperty("os.name", "").startsWith("Windows")