# HG changeset patch # User wenzelm # Date 1379004641 -7200 # Node ID 8533b4cb8dd74b8ab1f62de8de686195e2e40e23 # Parent c0ad478abf50fa3878bcbe81a3a3fe6b319c6d71 more robust System.getProperty with default; diff -r c0ad478abf50 -r 8533b4cb8dd7 src/Pure/System/gui_setup.scala --- a/src/Pure/System/gui_setup.scala Thu Sep 12 15:37:09 2013 +0200 +++ b/src/Pure/System/gui_setup.scala Thu Sep 12 18:50:41 2013 +0200 @@ -44,7 +44,7 @@ // values text.append("JVM name: " + Platform.jvm_name + "\n") text.append("JVM platform: " + Platform.jvm_platform + "\n") - text.append("JVM home: " + java.lang.System.getProperty("java.home") + "\n") + text.append("JVM home: " + java.lang.System.getProperty("java.home", "") + "\n") try { Isabelle_System.init() if (Platform.is_windows) diff -r c0ad478abf50 -r 8533b4cb8dd7 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Sep 12 15:37:09 2013 +0200 +++ b/src/Pure/System/isabelle_system.scala Thu Sep 12 18:50:41 2013 +0200 @@ -21,7 +21,7 @@ def jdk_home(): String = { - val java_home = System.getProperty("java.home") + val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && @@ -74,9 +74,9 @@ set_cygwin_root() val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())) - val user_home = System.getProperty("user.home") + val user_home = System.getProperty("user.home", "") val env = - if (user_home == null || env0.isDefinedAt("HOME")) env0 + if (user_home == "" || env0.isDefinedAt("HOME")) env0 else env0 + ("HOME" -> user_home) val system_home = @@ -84,8 +84,8 @@ else env.get("ISABELLE_HOME") match { case None | Some("") => - val path = System.getProperty("isabelle.home") - if (path == null || path == "") error("Unknown Isabelle home directory") + val path = System.getProperty("isabelle.home", "") + if (path == "") error("Unknown Isabelle home directory") else path case Some(path) => path } diff -r c0ad478abf50 -r 8533b4cb8dd7 src/Pure/System/platform.scala --- a/src/Pure/System/platform.scala Thu Sep 12 15:37:09 2013 +0200 +++ b/src/Pure/System/platform.scala Thu Sep 12 18:50:41 2013 +0200 @@ -16,8 +16,8 @@ { /* main OS variants */ - val is_macos = System.getProperty("os.name") == "Mac OS X" - val is_windows = System.getProperty("os.name").startsWith("Windows") + val is_macos = System.getProperty("os.name", "") == "Mac OS X" + val is_windows = System.getProperty("os.name", "").startsWith("Windows") /* Platform identifiers */ @@ -35,7 +35,7 @@ lazy val jvm_platform: String = { val arch = - System.getProperty("os.arch") match { + System.getProperty("os.arch", "") match { case X86() => "x86" case X86_64() => "x86_64" case Sparc() => "sparc" @@ -43,7 +43,7 @@ case _ => error("Failed to determine CPU architecture") } val os = - System.getProperty("os.name") match { + System.getProperty("os.name", "") match { case Solaris() => "solaris" case Linux() => "linux" case Darwin() => "darwin" @@ -56,6 +56,6 @@ /* JVM name */ - val jvm_name: String = System.getProperty("java.vm.name") + val jvm_name: String = System.getProperty("java.vm.name", "") } diff -r c0ad478abf50 -r 8533b4cb8dd7 src/Tools/jEdit/src/scala_console.scala --- a/src/Tools/jEdit/src/scala_console.scala Thu Sep 12 15:37:09 2013 +0200 +++ b/src/Tools/jEdit/src/scala_console.scala Thu Sep 12 18:50:41 2013 +0200 @@ -48,10 +48,7 @@ else Nil val initial_class_path = - System.getProperty("java.class.path") match { - case null => Nil - case class_path => Library.space_explode(JFile.pathSeparatorChar, class_path) - } + Library.space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", "")) val path = initial_class_path :::