# HG changeset patch
# User wenzelm
# Date 1334399771 -7200
# Node ID 5a7903ba2dac0dead7ae5cc30d030eda98540380
# Parent  70fd47ca62e3a8e6e1de95fd9e967d1aa6dbdc33
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;

diff -r 70fd47ca62e3 -r 5a7903ba2dac NEWS
--- a/NEWS	Sat Apr 14 11:46:35 2012 +0200
+++ b/NEWS	Sat Apr 14 12:36:11 2012 +0200
@@ -664,6 +664,12 @@
   delsplits     ~> Splitter.del_split
 
 
+*** System ***
+
+* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name
+notation, which is useful for the jEdit file browser, for example.
+
+
 
 New in Isabelle2011-1 (October 2011)
 ------------------------------------
diff -r 70fd47ca62e3 -r 5a7903ba2dac lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sat Apr 14 11:46:35 2012 +0200
+++ b/lib/scripts/getsettings	Sat Apr 14 12:36:11 2012 +0200
@@ -11,6 +11,21 @@
 
 ISABELLE_SETTINGS_PRESENT=true
 
+#JVM path wrapper
+if [ "$OSTYPE" = cygwin ]
+then
+  ISABELLE_HOME_WINDOWS="$(cygpath -d "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
+  ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
+
+  CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
+  function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
+  THIS_CYGWIN="$(jvmpath "/")"
+else
+  function jvmpath() { echo "$@"; }
+  CLASSPATH="$CLASSPATH"
+fi
+HOME_JVM="$HOME"
+
 export ISABELLE_HOME
 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
 then
@@ -53,17 +68,6 @@
   echo "$RESULT"
 }
 
-#JVM path wrapper
-if [ "$OSTYPE" = cygwin ]; then
-  CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
-  function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
-  THIS_CYGWIN="$(jvmpath "/")"
-else
-  function jvmpath() { echo "$@"; }
-  CLASSPATH="$CLASSPATH"
-fi
-HOME_JVM="$HOME"
-
 #shared library convenience
 function librarypath () {
   for X in "$@"