more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
authorwenzelm
Sat Apr 14 12:36:11 2012 +0200 (2012-04-14)
changeset 474615a7903ba2dac
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
     1.1 --- a/NEWS	Sat Apr 14 11:46:35 2012 +0200
     1.2 +++ b/NEWS	Sat Apr 14 12:36:11 2012 +0200
     1.3 @@ -664,6 +664,12 @@
     1.4    delsplits     ~> Splitter.del_split
     1.5  
     1.6  
     1.7 +*** System ***
     1.8 +
     1.9 +* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name
    1.10 +notation, which is useful for the jEdit file browser, for example.
    1.11 +
    1.12 +
    1.13  
    1.14  New in Isabelle2011-1 (October 2011)
    1.15  ------------------------------------
     2.1 --- a/lib/scripts/getsettings	Sat Apr 14 11:46:35 2012 +0200
     2.2 +++ b/lib/scripts/getsettings	Sat Apr 14 12:36:11 2012 +0200
     2.3 @@ -11,6 +11,21 @@
     2.4  
     2.5  ISABELLE_SETTINGS_PRESENT=true
     2.6  
     2.7 +#JVM path wrapper
     2.8 +if [ "$OSTYPE" = cygwin ]
     2.9 +then
    2.10 +  ISABELLE_HOME_WINDOWS="$(cygpath -d "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
    2.11 +  ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
    2.12 +
    2.13 +  CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    2.14 +  function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
    2.15 +  THIS_CYGWIN="$(jvmpath "/")"
    2.16 +else
    2.17 +  function jvmpath() { echo "$@"; }
    2.18 +  CLASSPATH="$CLASSPATH"
    2.19 +fi
    2.20 +HOME_JVM="$HOME"
    2.21 +
    2.22  export ISABELLE_HOME
    2.23  if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
    2.24  then
    2.25 @@ -53,17 +68,6 @@
    2.26    echo "$RESULT"
    2.27  }
    2.28  
    2.29 -#JVM path wrapper
    2.30 -if [ "$OSTYPE" = cygwin ]; then
    2.31 -  CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    2.32 -  function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
    2.33 -  THIS_CYGWIN="$(jvmpath "/")"
    2.34 -else
    2.35 -  function jvmpath() { echo "$@"; }
    2.36 -  CLASSPATH="$CLASSPATH"
    2.37 -fi
    2.38 -HOME_JVM="$HOME"
    2.39 -
    2.40  #shared library convenience
    2.41  function librarypath () {
    2.42    for X in "$@"