# 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 :::