tuned -- use existing operation;
authorwenzelm
Sat, 09 Jun 2018 13:19:57 +0200
changeset 68409 c8c3136e3ba7
parent 68408 9a2453622596
child 68410 4e27f5c361d2
tuned -- use existing operation;
src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Jun 07 22:46:40 2018 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jun 09 13:19:57 2018 +0200
@@ -32,13 +32,10 @@
   def bootstrap_directory(
     preference: String, envar: String, property: String, description: String): String =
   {
-    def check(s: String): Option[String] =
-      if (s != null && s != "") Some(s) else None
-
     val value =
-      check(preference) orElse  // explicit argument
-      check(System.getenv(envar)) orElse  // e.g. inherited from running isabelle tool
-      check(System.getProperty(property)) getOrElse  // e.g. via JVM application boot process
+      proper_string(preference) orElse  // explicit argument
+      proper_string(System.getenv(envar)) orElse  // e.g. inherited from running isabelle tool
+      proper_string(System.getProperty(property)) getOrElse  // e.g. via JVM application boot process
       error("Unknown " + description + " directory")
 
     if ((new JFile(value)).isDirectory) value