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