more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
authorwenzelm
Sat, 14 Apr 2012 12:36:11 +0200
changeset 47461 5a7903ba2dac
parent 47460 70fd47ca62e3
child 47462 8f85051693d1
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
NEWS
lib/scripts/getsettings
--- 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)
 ------------------------------------
--- 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 "$@"