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