--- a/src/Pure/System/gui_setup.scala Mon Apr 29 15:47:42 2013 +0200
+++ b/src/Pure/System/gui_setup.scala Mon Apr 29 17:01:13 2013 +0200
@@ -42,13 +42,13 @@
contents = panel
// values
- if (Platform.is_windows)
- text.append("Cygwin root: " + Isabelle_System.cygwin_root() + "\n")
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")
try {
Isabelle_System.init()
+ if (Platform.is_windows)
+ text.append("Cygwin root: " + Isabelle_System.get_cygwin_root() + "\n")
text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n")
val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
--- a/src/Pure/System/isabelle_system.scala Mon Apr 29 15:47:42 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon Apr 29 17:01:13 2013 +0200
@@ -29,14 +29,15 @@
else java_home
}
- def cygwin_root(): String =
+ private def find_cygwin_root(cygwin_root0: String = ""): String =
{
require(Platform.is_windows)
val cygwin_root1 = System.getenv("CYGWIN_ROOT")
val cygwin_root2 = System.getProperty("cygwin.root")
- if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
+ 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")
}
@@ -54,54 +55,61 @@
}
/*
- isabelle_home precedence:
- (1) this_isabelle_home as explicit argument
+ 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(this_isabelle_home: String = null): Unit = synchronized {
+ def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized {
if (_settings.isEmpty) {
import scala.collection.JavaConversions._
- val settings =
+ def set_cygwin_root()
{
- val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home()))
-
- val user_home = System.getProperty("user.home")
- val env =
- if (user_home == null || env0.isDefinedAt("HOME")) env0
- else env0 + ("HOME" -> user_home)
+ if (Platform.is_windows)
+ _settings = Some(_settings.getOrElse(Map.empty) +
+ ("CYGWIN_ROOT" -> find_cygwin_root(cygwin_root)))
+ }
- val isabelle_home =
- if (this_isabelle_home != null) this_isabelle_home
- else
- env.get("ISABELLE_HOME") match {
- case None | Some("") =>
- val path = System.getProperty("isabelle.home")
- if (path == null || path == "") error("Unknown Isabelle home directory")
- else path
- case Some(path) => path
- }
+ set_cygwin_root()
+ val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home()))
+
+ val user_home = System.getProperty("user.home")
+ val env =
+ if (user_home == null || env0.isDefinedAt("HOME")) env0
+ else env0 + ("HOME" -> user_home)
- File.with_tmp_file("settings") { dump =>
- val shell_prefix =
- if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash", "-l")
- else Nil
- val cmdline =
- shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
- val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
- if (rc != 0) error(output)
+ 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 == null || path == "") error("Unknown Isabelle home directory")
+ else path
+ case Some(path) => path
+ }
- val entries =
- (for (entry <- File.read(dump) split "\0" if entry != "") yield {
- val i = entry.indexOf('=')
- if (i <= 0) (entry -> "")
- else (entry.substring(0, i) -> entry.substring(i + 1))
- }).toMap
- entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
- }
- }
+ val settings =
+ File.with_tmp_file("settings") { dump =>
+ val shell_prefix =
+ if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l")
+ else Nil
+ val cmdline =
+ shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
+ val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
+ if (rc != 0) error(output)
+
+ val entries =
+ (for (entry <- File.read(dump) split "\0" if entry != "") yield {
+ val i = entry.indexOf('=')
+ if (i <= 0) (entry -> "")
+ else (entry.substring(0, i) -> entry.substring(i + 1))
+ }).toMap
+ entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
+ }
_settings = Some(settings)
+ set_cygwin_root()
}
}
@@ -116,6 +124,8 @@
if (value != "") value else error("Undefined environment variable: " + name)
}
+ def get_cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
+
/** file-system operations **/
@@ -138,7 +148,7 @@
result_path ++= root
rest
case path if path.startsWith("/") =>
- result_path ++= cygwin_root()
+ result_path ++= get_cygwin_root()
path
case path => path
}
@@ -158,7 +168,7 @@
def posix_path(jvm_path: String): String =
if (Platform.is_windows) {
val Platform_Root = new Regex("(?i)" +
- Pattern.quote(cygwin_root()) + """(?:\\+|\z)(.*)""")
+ Pattern.quote(get_cygwin_root()) + """(?:\\+|\z)(.*)""")
val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
jvm_path.replace('/', '\\') match {
@@ -257,7 +267,7 @@
def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
{
val cmdline =
- if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ++ args
+ if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ++ args
else args
val env1 = if (env == null) settings else settings ++ env
raw_execute(cwd, env1, redirect, cmdline: _*)