src/Pure/System/platform.scala
author wenzelm
Fri, 05 Feb 2010 19:48:13 +0100
changeset 35002 fbb40a1091ea
parent 31828 31584cf201cc
child 36195 9c098598db2a
permissions -rw-r--r--
try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
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
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    22
  /* Isabelle platform identifiers */
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")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    27
  private val Cygwin = new Regex("Windows.*")
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
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    34
  // main default, optional 64bit variant
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    35
  val defaults: Option[(String, Option[String])] =
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    36
  {
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    37
    (java.lang.System.getProperty("os.name") match {
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    38
      case Solaris() => Some("solaris")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    39
      case Linux() => Some("linux")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    40
      case Darwin() => Some("darwin")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    41
      case Cygwin() => Some("cygwin")
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    42
      case _ => None
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    43
    }) match {
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    44
      case Some(name) =>
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    45
        java.lang.System.getProperty("os.arch") match {
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    46
          case X86() => Some(("x86-" + name, None))
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    47
          case X86_64() => Some(("x86-" + name, if (is_windows) None else Some("x86_64-" + name)))
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    48
          case Sparc() => Some(("sparc-" + name, None))
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    49
          case PPC() => Some(("ppc-" + name, None))
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    50
        }
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    51
      case None => None
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    52
    }
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
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    56
  /* Swing look-and-feel */
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    57
35002
fbb40a1091ea try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
wenzelm
parents: 31828
diff changeset
    58
  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
    59
    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
    60
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    61
  def look_and_feel(): String =
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    62
  {
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    63
    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
    64
    else
fbb40a1091ea try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
wenzelm
parents: 31828
diff changeset
    65
      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
    66
      UIManager.getCrossPlatformLookAndFeelClassName()
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    67
  }
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    68
}
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    69