src/Pure/System/platform.scala
author wenzelm
Mon, 28 Nov 2011 22:18:19 +0100
changeset 45667 546d78f0d81f
parent 43520 cec9b95fa35d
child 45673 cd41e3903fbf
permissions -rw-r--r--
explicit indication of modules for independent Scala library;
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
45667
546d78f0d81f explicit indication of modules for independent Scala library;
wenzelm
parents: 43520
diff changeset
     2
    Module:     Library
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     4
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     5
Raw platform identification.
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     6
*/
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     7
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     8
package isabelle
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     9
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 41381
diff changeset
    10
import java.lang.System
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    11
import javax.swing.UIManager
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    12
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    13
import scala.util.matching.Regex
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    14
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    15
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    16
object Platform
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    17
{
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    18
  /* main OS variants */
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    19
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    20
  val is_macos = System.getProperty("os.name") == "Mac OS X"
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    21
  val is_windows = System.getProperty("os.name").startsWith("Windows")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    22
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    23
36195
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    24
  /* Platform identifiers */
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    25
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    26
  private val Solaris = new Regex("SunOS|Solaris")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    27
  private val Linux = new Regex("Linux")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    28
  private val Darwin = new Regex("Mac OS X")
36195
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    29
  private val Windows = new Regex("Windows.*")
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    30
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    31
  private val X86 = new Regex("i.86|x86")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    32
  private val X86_64 = new Regex("amd64|x86_64")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    33
  private val Sparc = new Regex("sparc")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    34
  private val PPC = new Regex("PowerPC|ppc")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    35
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
    36
  lazy val jvm_platform: String =
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    37
  {
36195
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    38
    val arch =
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 41381
diff changeset
    39
      System.getProperty("os.arch") match {
36195
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    40
        case X86() => "x86"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    41
        case X86_64() => "x86_64"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    42
        case Sparc() => "sparc"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    43
        case PPC() => "ppc"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    44
        case _ => error("Failed to determine CPU architecture")
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    45
      }
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    46
    val os =
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 41381
diff changeset
    47
      System.getProperty("os.name") match {
36195
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    48
        case Solaris() => "solaris"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    49
        case Linux() => "linux"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    50
        case Darwin() => "darwin"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    51
        case Windows() => "windows"
9c098598db2a system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents: 35002
diff changeset
    52
        case _ => error("Failed to determine operating system platform")
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
    arch + "-" + os
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    55
  }
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    56
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    57
41381
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 36786
diff changeset
    58
  /* JVM name */
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 36786
diff changeset
    59
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 41381
diff changeset
    60
  val jvm_name: String = System.getProperty("java.vm.name")
41381
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 36786
diff changeset
    61
  val is_hotspot: Boolean = jvm_name.startsWith("Java HotSpot")
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 36786
diff changeset
    62
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 36786
diff changeset
    63
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    64
  /* Swing look-and-feel */
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    65
35002
fbb40a1091ea try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
wenzelm
parents: 31828
diff changeset
    66
  private def find_laf(name: String): Option[String] =
fbb40a1091ea try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
wenzelm
parents: 31828
diff changeset
    67
    UIManager.getInstalledLookAndFeels().find(_.getName == name).map(_.getClassName)
fbb40a1091ea try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
wenzelm
parents: 31828
diff changeset
    68
36786
b7a62e7dec00 more convenient look-and-feel setup;
wenzelm
parents: 36205
diff changeset
    69
  def get_laf(): String =
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    70
  {
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    71
    if (is_windows || is_macos) UIManager.getSystemLookAndFeelClassName()
35002
fbb40a1091ea try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
wenzelm
parents: 31828
diff changeset
    72
    else
fbb40a1091ea try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
wenzelm
parents: 31828
diff changeset
    73
      find_laf("Nimbus") orElse find_laf("GTK+") getOrElse
fbb40a1091ea try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
wenzelm
parents: 31828
diff changeset
    74
      UIManager.getCrossPlatformLookAndFeelClassName()
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    75
  }
36786
b7a62e7dec00 more convenient look-and-feel setup;
wenzelm
parents: 36205
diff changeset
    76
b7a62e7dec00 more convenient look-and-feel setup;
wenzelm
parents: 36205
diff changeset
    77
  def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    78
}
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    79