--- a/src/Pure/System/isabelle_system.scala Wed Sep 30 14:49:39 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Sep 30 20:02:39 2015 +0200
@@ -29,17 +29,20 @@
else java_home
}
- private def find_cygwin_root(cygwin_root0: String = ""): String =
+ def bootstrap_directory(
+ preference: String, envar: String, property: String, description: String): String =
{
- require(Platform.is_windows)
+ def check(s: String): Option[String] =
+ if (s != null && s != "") Some(s) else None
- val cygwin_root1 = System.getenv("CYGWIN_ROOT")
- val cygwin_root2 = System.getProperty("cygwin.root")
+ 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
+ error("Unknown " + description + " directory")
- if (cygwin_root0 != null && cygwin_root0 != "") cygwin_root0
- else if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
- else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
- else error("Cannot determine Cygwin root directory")
+ if ((new JFile(value)).isDirectory) value
+ else error("Bad " + description + " directory " + quote(value))
}
@@ -54,21 +57,22 @@
_settings.get
}
- /*
- Isabelle home precedence:
- (1) isabelle_home as explicit argument
- (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
- (3) isabelle.home system property (e.g. via JVM application boot process)
- */
def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized {
if (_settings.isEmpty) {
import scala.collection.JavaConversions._
+ val isabelle_home1 =
+ bootstrap_directory(isabelle_home, "ISABELLE_HOME", "isabelle.home", "Isabelle home")
+
+ val cygwin_root1 =
+ if (Platform.is_windows)
+ bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
+ else ""
+
def set_cygwin_root()
{
if (Platform.is_windows)
- _settings = Some(_settings.getOrElse(Map.empty) +
- ("CYGWIN_ROOT" -> find_cygwin_root(cygwin_root)))
+ _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
}
set_cygwin_root()
@@ -81,7 +85,7 @@
{
val temp_windows =
{
- val temp = System.getenv("TEMP")
+ val temp = if (Platform.is_windows) System.getenv("TEMP") else null
if (temp != null && temp.contains('\\')) temp else ""
}
val user_home = System.getProperty("user.home", "")
@@ -95,27 +99,15 @@
"ISABELLE_APP" -> "true")
}
- val system_home =
- if (isabelle_home != null && isabelle_home != "") isabelle_home
- else
- env.get("ISABELLE_HOME") match {
- case None | Some("") =>
- val path = System.getProperty("isabelle.home", "")
- if (path == "") error("Unknown Isabelle home directory")
- else path
- case Some(path) => path
- }
-
val settings =
{
val dump = JFile.createTempFile("settings", null)
dump.deleteOnExit
try {
val shell_prefix =
- if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l")
- else Nil
+ if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l") else Nil
val cmdline =
- shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
+ shell_prefix ::: List(isabelle_home1 + "/bin/isabelle", "getenv", "-d", dump.toString)
val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
if (rc != 0) error(output)
@@ -146,7 +138,7 @@
else error("Undefined Isabelle environment variable: " + quote(name))
}
- def get_cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
+ def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
@@ -218,7 +210,7 @@
def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
{
val cmdline =
- if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ::: args.toList
+ if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ::: args.toList
else args
val env1 = if (env == null) settings else settings ++ env
raw_execute(cwd, env1, redirect, cmdline: _*)
@@ -298,7 +290,7 @@
def kill(signal: String, group_pid: String): (String, Int) =
{
val bash =
- if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\bash.exe")
+ if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
val cmdline = bash ::: List("-c", "kill -" + signal + " -" + group_pid)
process_output(raw_execute(null, null, true, cmdline: _*))