# HG changeset patch # User wenzelm # Date 1293015917 -3600 # Node ID 77990a6cd558448bfca57be4366fedcc97ee0f3e # Parent 92237dee0f29dfe31b0e5c7af8edb272ef7be5df more explicit jvm_name; diff -r 92237dee0f29 -r 77990a6cd558 src/Pure/System/gui_setup.scala --- a/src/Pure/System/gui_setup.scala Wed Dec 22 11:52:57 2010 +0100 +++ b/src/Pure/System/gui_setup.scala Wed Dec 22 12:05:17 2010 +0100 @@ -39,7 +39,7 @@ // values if (Platform.is_windows) text.append("Cygwin root: " + Cygwin.check_root() + "\n") - text.append("JVM name: " + System.getProperty("java.vm.name") + "\n") + text.append("JVM name: " + Platform.jvm_name + "\n") text.append("JVM platform: " + Platform.jvm_platform + "\n") try { val isabelle_system = new Isabelle_System diff -r 92237dee0f29 -r 77990a6cd558 src/Pure/System/platform.scala --- a/src/Pure/System/platform.scala Wed Dec 22 11:52:57 2010 +0100 +++ b/src/Pure/System/platform.scala Wed Dec 22 12:05:17 2010 +0100 @@ -53,6 +53,12 @@ } + /* JVM name */ + + val jvm_name: String = java.lang.System.getProperty("java.vm.name") + val is_hotspot: Boolean = jvm_name.startsWith("Java HotSpot") + + /* Swing look-and-feel */ private def find_laf(name: String): Option[String] =