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