# HG changeset patch
# User wenzelm
# Date 1528543197 -7200
# Node ID c8c3136e3ba7f43e0d6a3e16e43f7ac405656999
# Parent  9a24536225965c99bd9142fe91d54fb4c4cda504
tuned -- use existing operation;

diff -r 9a2453622596 -r c8c3136e3ba7 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