# HG changeset patch
# User wenzelm
# Date 1443639914 -7200
# Node ID 876e7eae22becc3e569bc15999898d6296088fbc
# Parent  ca76026ed7cc0ce04c83df33da016495b2df12e8
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);

diff -r ca76026ed7cc -r 876e7eae22be Admin/Windows/launch4j/isabelle.xml
--- a/Admin/Windows/launch4j/isabelle.xml	Wed Sep 30 20:48:59 2015 +0200
+++ b/Admin/Windows/launch4j/isabelle.xml	Wed Sep 30 21:05:14 2015 +0200
@@ -30,7 +30,7 @@
     <maxVersion></maxVersion>
     <jdkPreference>jdkOnly</jdkPreference>
     <runtimeBits>{PLATFORM_BITS}</runtimeBits>
-    <opt>-Disabelle.home=&quot;%EXEDIR%&quot; -Dcygwin.root=&quot;%EXEDIR%\\contrib\\cygwin&quot;</opt>
+    <opt>-Disabelle.root=&quot;%EXEDIR%&quot; -Dcygwin.root=&quot;%EXEDIR%\\contrib\\cygwin&quot;</opt>
   </jre>
   <splash>
     <file>{SPLASH}</file>
diff -r ca76026ed7cc -r 876e7eae22be lib/scripts/getsettings
--- a/lib/scripts/getsettings	Wed Sep 30 20:48:59 2015 +0200
+++ b/lib/scripts/getsettings	Wed Sep 30 21:05:14 2015 +0200
@@ -38,6 +38,7 @@
 
   function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
   CYGWIN_ROOT="$(jvmpath "/")"
+  ISABELLE_ROOT="$(jvmpath "$ISABELLE_HOME")"
 
   ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
   unset CLASSPATH
@@ -46,6 +47,8 @@
     USER_HOME="$HOME"
   fi
 
+  ISABELLE_ROOT="$ISABELLE_HOME"
+
   function jvmpath() { echo "$@"; }
 
   ISABELLE_CLASSPATH="$CLASSPATH"
diff -r ca76026ed7cc -r 876e7eae22be src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala	Wed Sep 30 20:48:59 2015 +0200
+++ b/src/Pure/System/cygwin.scala	Wed Sep 30 21:05:14 2015 +0200
@@ -17,13 +17,13 @@
 {
   /* init (e.g. after extraction via 7zip) */
 
-  def init(isabelle_home: String, cygwin_root: String)
+  def init(isabelle_root: String, cygwin_root: String)
   {
     require(Platform.is_windows)
 
     def execute(args: String*)
     {
-      val cwd = new JFile(isabelle_home)
+      val cwd = new JFile(isabelle_root)
       val env = Map("CYGWIN" -> "nodosfilewarning")
       val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
       val (output, rc) = Isabelle_System.process_output(proc)
@@ -44,7 +44,7 @@
         list match {
           case Nil | List("") =>
           case link :: content :: rest =>
-            val path = (new JFile(isabelle_home, link)).toPath
+            val path = (new JFile(isabelle_root, link)).toPath
 
             val writer = Files.newBufferedWriter(path, UTF8.charset)
             try { writer.write("!<symlink>" + content + "\u0000") }
diff -r ca76026ed7cc -r 876e7eae22be src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Sep 30 20:48:59 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Sep 30 21:05:14 2015 +0200
@@ -57,12 +57,12 @@
     _settings.get
   }
 
-  def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized {
+  def init(isabelle_root: 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 isabelle_root1 =
+        bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
 
       val cygwin_root1 =
         if (Platform.is_windows)
@@ -104,11 +104,13 @@
         val dump = JFile.createTempFile("settings", null)
         dump.deleteOnExit
         try {
-          val shell_prefix =
+          val cmd1 =
             if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l") else Nil
-          val cmdline =
-            shell_prefix ::: List(isabelle_home1 + "/bin/isabelle", "getenv", "-d", dump.toString)
-          val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
+          val cmd2 =
+            List(isabelle_root1 + JFile.separator + "bin" + JFile.separator + "isabelle",
+              "getenv", "-d", dump.toString)
+
+          val (output, rc) = process_output(raw_execute(null, env, true, (cmd1 ::: cmd2): _*))
           if (rc != 0) error(output)
 
           val entries =