src/Pure/System/platform.scala
author wenzelm
Thu, 06 Dec 2018 14:25:27 +0100
changeset 69410 c071fcec4323
parent 69112 5b749aa452c6
child 69726 461f0615faa3
permissions -rw-r--r--
more explicit Platform.Family;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/platform.scala
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     3
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
     4
System platform identification.
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     5
*/
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     6
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     7
package isabelle
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     8
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
     9
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    10
object Platform
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    11
{
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    12
  /* platform family */
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    13
64493
a2eebcc8bb69 clarified platform selection;
wenzelm
parents: 64370
diff changeset
    14
  val is_linux = System.getProperty("os.name", "") == "Linux"
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 51617
diff changeset
    15
  val is_macos = System.getProperty("os.name", "") == "Mac OS X"
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 51617
diff changeset
    16
  val is_windows = System.getProperty("os.name", "").startsWith("Windows")
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    17
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    18
  def family: Family.Value =
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    19
    if (is_linux) Family.linux
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    20
    else if (is_macos) Family.macos
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    21
    else if (is_windows) Family.windows
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    22
    else error("Failed to determine current platform family")
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    23
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    24
  object Family extends Enumeration
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    25
  {
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    26
    val linux, macos, windows = Value
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    27
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    28
    def unapply(name: String): Option[Value] =
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    29
      try { Some(withName(name)) }
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    30
      catch { case _: NoSuchElementException => None }
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    31
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    32
    def parse(name: String): Value =
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    33
      unapply(name) getOrElse error("Bad platform family: " + quote(name))
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    34
  }
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    35
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    36
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    37
  /* platform identifiers */
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    38
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    39
  private val Linux = """Linux""".r
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    40
  private val Darwin = """Mac OS X""".r
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    41
  private val Windows = """Windows.*""".r
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    42
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    43
  private val X86 = """i.86|x86""".r
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    44
  private val X86_64 = """amd64|x86_64""".r
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    45
36205
e86d9a10e982 check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
wenzelm
parents: 36195
diff changeset
    46
  lazy val jvm_platform: String =
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    47
  {
36195
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    48
    val arch =
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 51617
diff changeset
    49
      System.getProperty("os.arch", "") match {
36195
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    50
        case X86() => "x86"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    51
        case X86_64() => "x86_64"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    52
        case _ => error("Failed to determine CPU architecture")
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    53
      }
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    54
    val os =
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 51617
diff changeset
    55
      System.getProperty("os.name", "") match {
36195
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    56
        case Linux() => "linux"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    57
        case Darwin() => "darwin"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    58
        case Windows() => "windows"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    59
        case _ => error("Failed to determine operating system platform")
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    60
      }
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    61
    arch + "-" + os
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    62
  }
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    63
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    64
61001
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    65
  /* JVM version */
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    66
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    67
  private val Version = """1\.(\d+)\.0_(\d+)""".r
61001
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    68
  lazy val jvm_version =
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    69
    System.getProperty("java.version") match {
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    70
      case Version(a, b) => a + "u" + b
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    71
      case a => a
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    72
    }
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    73
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    74
41381
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 36786
diff changeset
    75
  /* JVM name */
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 36786
diff changeset
    76
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 51617
diff changeset
    77
  val jvm_name: String = System.getProperty("java.vm.name", "")
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    78
}