author | wenzelm |
Tue, 29 Nov 2011 21:29:53 +0100 | |
changeset 45673 | cd41e3903fbf |
parent 45667 | 546d78f0d81f |
child 46117 | edd50ec8d471 |
permissions | -rw-r--r-- |
31825 | 1 |
/* Title: Pure/System/platform.scala |
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset
|
2 |
Module: PIDE |
31825 | 3 |
Author: Makarius |
4 |
||
5 |
Raw platform identification. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
41381
diff
changeset
|
10 |
import java.lang.System |
31828 | 11 |
import javax.swing.UIManager |
12 |
||
31825 | 13 |
import scala.util.matching.Regex |
14 |
||
15 |
||
16 |
object Platform |
|
17 |
{ |
|
31828 | 18 |
/* main OS variants */ |
19 |
||
31825 | 20 |
val is_macos = System.getProperty("os.name") == "Mac OS X" |
21 |
val is_windows = System.getProperty("os.name").startsWith("Windows") |
|
22 |
||
31828 | 23 |
|
36195
9c098598db2a
system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents:
35002
diff
changeset
|
24 |
/* Platform identifiers */ |
31828 | 25 |
|
31825 | 26 |
private val Solaris = new Regex("SunOS|Solaris") |
27 |
private val Linux = new Regex("Linux") |
|
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 | 30 |
|
31 |
private val X86 = new Regex("i.86|x86") |
|
32 |
private val X86_64 = new Regex("amd64|x86_64") |
|
33 |
private val Sparc = new Regex("sparc") |
|
34 |
private val PPC = new Regex("PowerPC|ppc") |
|
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 | 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 | 55 |
} |
31828 | 56 |
|
57 |
||
41381 | 58 |
/* JVM name */ |
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 | 61 |
val is_hotspot: Boolean = jvm_name.startsWith("Java HotSpot") |
62 |
||
63 |
||
31828 | 64 |
/* Swing look-and-feel */ |
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 | 69 |
def get_laf(): String = |
31828 | 70 |
{ |
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 | 75 |
} |
36786 | 76 |
|
77 |
def init_laf(): Unit = UIManager.setLookAndFeel(get_laf()) |
|
31825 | 78 |
} |
79 |