1.1 --- a/NEWS Sun Apr 22 11:05:04 2012 +0200
1.2 +++ b/NEWS Sun Apr 22 14:30:18 2012 +0200
1.3 @@ -869,6 +869,14 @@
1.4
1.5 *** System ***
1.6
1.7 +* USER_HOME settings variable points to cross-platform user home
1.8 +directory, which coincides with HOME on POSIX systems only. Likewise,
1.9 +the Isabelle path specification "~" now expands to $USER_HOME, instead
1.10 +of former $HOME. A different default for USER_HOME may be set
1.11 +explicitly in shell environment, before Isabelle settings are
1.12 +evaluated. Minor INCOMPATIBILITY: need to adapt Isabelle path where
1.13 +the generic user home was intended.
1.14 +
1.15 * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar
1.16 (not just JRE).
1.17
2.1 --- a/doc-src/IsarRef/Thy/Misc.thy Sun Apr 22 11:05:04 2012 +0200
2.2 +++ b/doc-src/IsarRef/Thy/Misc.thy Sun Apr 22 14:30:18 2012 +0200
2.3 @@ -143,9 +143,9 @@
2.4 %FIXME proper place (!?)
2.5 Isabelle file specification may contain path variables (e.g.\
2.6 @{verbatim "$ISABELLE_HOME"}) that are expanded accordingly. Note
2.7 - that @{verbatim "~"} abbreviates @{verbatim "$HOME"}, and @{verbatim
2.8 - "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}. The general syntax
2.9 - for path specifications follows POSIX conventions.
2.10 + that @{verbatim "~"} abbreviates @{verbatim "$USER_HOME"}, and
2.11 + @{verbatim "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}. The
2.12 + general syntax for path specifications follows POSIX conventions.
2.13 *}
2.14
2.15 end
3.1 --- a/doc-src/IsarRef/Thy/document/Misc.tex Sun Apr 22 11:05:04 2012 +0200
3.2 +++ b/doc-src/IsarRef/Thy/document/Misc.tex Sun Apr 22 14:30:18 2012 +0200
3.3 @@ -256,8 +256,9 @@
3.4 %FIXME proper place (!?)
3.5 Isabelle file specification may contain path variables (e.g.\
3.6 \verb|$ISABELLE_HOME|) that are expanded accordingly. Note
3.7 - that \verb|~| abbreviates \verb|$HOME|, and \verb|~~| abbreviates \verb|$ISABELLE_HOME|. The general syntax
3.8 - for path specifications follows POSIX conventions.%
3.9 + that \verb|~| abbreviates \verb|$USER_HOME|, and
3.10 + \verb|~~| abbreviates \verb|$ISABELLE_HOME|. The
3.11 + general syntax for path specifications follows POSIX conventions.%
3.12 \end{isamarkuptext}%
3.13 \isamarkuptrue%
3.14 %
4.1 --- a/doc-src/System/Thy/Basics.thy Sun Apr 22 11:05:04 2012 +0200
4.2 +++ b/doc-src/System/Thy/Basics.thy Sun Apr 22 14:30:18 2012 +0200
4.3 @@ -96,7 +96,7 @@
4.4 exists) is run in the same way as the site default settings. Note
4.5 that the variable @{setting ISABELLE_HOME_USER} has already been set
4.6 before --- usually to something like @{verbatim
4.7 - "$HOME/.isabelle/IsabelleXXXX"}.
4.8 + "$USER_HOME/.isabelle/IsabelleXXXX"}.
4.9
4.10 Thus individual users may override the site-wide defaults. See also
4.11 file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
4.12 @@ -149,19 +149,24 @@
4.13
4.14 \begin{description}
4.15
4.16 - \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the
4.17 - location of the top-level Isabelle distribution directory. This is
4.18 - automatically determined from the Isabelle executable that has been
4.19 - invoked. Do not attempt to set @{setting ISABELLE_HOME} yourself
4.20 - from the shell!
4.21 + \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the
4.22 + cross-platform user home directory. On Unix systems this is usually
4.23 + the same as @{setting HOME}, but on Windows it is the regular home
4.24 + directory of the user, not the one of within the Cygwin root
4.25 + file-system.
4.26 +
4.27 + \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the
4.28 + top-level Isabelle distribution directory. This is automatically
4.29 + determined from the Isabelle executable that has been invoked. Do
4.30 + not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
4.31
4.32 \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
4.33 counterpart of @{setting ISABELLE_HOME}. The default value is
4.34 - relative to @{verbatim "$HOME/.isabelle"}, under rare circumstances
4.35 - this may be changed in the global setting file. Typically, the
4.36 - @{setting ISABELLE_HOME_USER} directory mimics @{setting
4.37 - ISABELLE_HOME} to some extend. In particular, site-wide defaults may
4.38 - be overridden by a private @{verbatim
4.39 + relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
4.40 + circumstances this may be changed in the global setting file.
4.41 + Typically, the @{setting ISABELLE_HOME_USER} directory mimics
4.42 + @{setting ISABELLE_HOME} to some extend. In particular, site-wide
4.43 + defaults may be overridden by a private @{verbatim
4.44 "$ISABELLE_HOME_USER/etc/settings"}.
4.45
4.46 \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
5.1 --- a/doc-src/System/Thy/document/Basics.tex Sun Apr 22 11:05:04 2012 +0200
5.2 +++ b/doc-src/System/Thy/document/Basics.tex Sun Apr 22 14:30:18 2012 +0200
5.3 @@ -114,7 +114,7 @@
5.4 \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
5.5 exists) is run in the same way as the site default settings. Note
5.6 that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} has already been set
5.7 - before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
5.8 + before --- usually to something like \verb|$USER_HOME/.isabelle/IsabelleXXXX|.
5.9
5.10 Thus individual users may override the site-wide defaults. See also
5.11 file \verb|$ISABELLE_HOME/etc/user-settings.sample| in the
5.12 @@ -167,18 +167,23 @@
5.13
5.14 \begin{description}
5.15
5.16 - \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is the
5.17 - location of the top-level Isabelle distribution directory. This is
5.18 - automatically determined from the Isabelle executable that has been
5.19 - invoked. Do not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} yourself
5.20 - from the shell!
5.21 + \item[\indexdef{}{setting}{USER\_HOME}\hypertarget{setting.USER-HOME}{\hyperlink{setting.USER-HOME}{\mbox{\isa{\isatt{USER{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] Is the cross-platform
5.22 + user home directory. On Unix systems this is usually the same as
5.23 + \hyperlink{setting.HOME}{\mbox{\isa{\isatt{HOME}}}}, but on Windows it is the regular home directory of
5.24 + the, not the one of within the Cygwin root file-system.
5.25 +
5.26 + \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is the location of the
5.27 + top-level Isabelle distribution directory. This is automatically
5.28 + determined from the Isabelle executable that has been invoked. Do
5.29 + not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} yourself from the shell!
5.30
5.31 \item[\indexdef{}{setting}{ISABELLE\_HOME\_USER}\hypertarget{setting.ISABELLE-HOME-USER}{\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}}}] is the user-specific
5.32 counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}. The default value is
5.33 - relative to \verb|$HOME/.isabelle|, under rare circumstances
5.34 - this may be changed in the global setting file. Typically, the
5.35 - \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} to some extend. In particular, site-wide defaults may
5.36 - be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
5.37 + relative to \verb|$USER_HOME/.isabelle|, under rare
5.38 + circumstances this may be changed in the global setting file.
5.39 + Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} directory mimics
5.40 + \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} to some extend. In particular, site-wide
5.41 + defaults may be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
5.42
5.43 \item[\indexdef{}{setting}{ISABELLE\_PLATFORM}\hypertarget{setting.ISABELLE-PLATFORM}{\hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is automatically
5.44 set to a symbolic identifier for the underlying hardware and
6.1 --- a/etc/settings Sun Apr 22 11:05:04 2012 +0200
6.2 +++ b/etc/settings Sun Apr 22 14:30:18 2012 +0200
6.3 @@ -93,7 +93,7 @@
6.4 ###
6.5
6.6 # The place for user configuration, heap files, etc.
6.7 -ISABELLE_HOME_USER="$HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
6.8 +ISABELLE_HOME_USER="$USER_HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
6.9
6.10 # Where to look for isabelle tools (multiple dirs separated by ':').
6.11 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
7.1 --- a/lib/scripts/getsettings Sun Apr 22 11:05:04 2012 +0200
7.2 +++ b/lib/scripts/getsettings Sun Apr 22 14:30:18 2012 +0200
7.3 @@ -11,9 +11,13 @@
7.4
7.5 ISABELLE_SETTINGS_PRESENT=true
7.6
7.7 -#JVM path wrapper
7.8 +#Cygwin vs Posix
7.9 if [ "$OSTYPE" = cygwin ]
7.10 then
7.11 + if [ -z "$USER_HOME" ]; then
7.12 + USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
7.13 + fi
7.14 +
7.15 ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
7.16 ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
7.17
7.18 @@ -21,10 +25,13 @@
7.19 function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
7.20 THIS_CYGWIN="$(jvmpath "/")"
7.21 else
7.22 + if [ -z "$USER_HOME" ]; then
7.23 + USER_HOME="$HOME"
7.24 + fi
7.25 +
7.26 function jvmpath() { echo "$@"; }
7.27 CLASSPATH="$CLASSPATH"
7.28 fi
7.29 -HOME_JVM="$HOME"
7.30
7.31 export ISABELLE_HOME
7.32 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
8.1 --- a/src/Pure/General/path.ML Sun Apr 22 11:05:04 2012 +0200
8.2 +++ b/src/Pure/General/path.ML Sun Apr 22 14:30:18 2012 +0200
8.3 @@ -127,7 +127,7 @@
8.4 local
8.5
8.6 fun explode_elem ".." = Parent
8.7 - | explode_elem "~" = Variable "HOME"
8.8 + | explode_elem "~" = Variable "USER_HOME"
8.9 | explode_elem "~~" = Variable "ISABELLE_HOME"
8.10 | explode_elem s =
8.11 (case raw_explode s of
9.1 --- a/src/Pure/General/path.scala Sun Apr 22 11:05:04 2012 +0200
9.2 +++ b/src/Pure/General/path.scala Sun Apr 22 14:30:18 2012 +0200
9.3 @@ -72,7 +72,7 @@
9.4
9.5 private def explode_elem(s: String): Elem =
9.6 if (s == "..") Parent
9.7 - else if (s == "~") Variable("HOME")
9.8 + else if (s == "~") Variable("USER_HOME")
9.9 else if (s == "~~") Variable("ISABELLE_HOME")
9.10 else if (s.startsWith("$")) variable_elem(s.substring(1))
9.11 else basic_elem(s)
10.1 --- a/src/Pure/System/isabelle_system.scala Sun Apr 22 11:05:04 2012 +0200
10.2 +++ b/src/Pure/System/isabelle_system.scala Sun Apr 22 14:30:18 2012 +0200
10.3 @@ -79,9 +79,7 @@
10.4 if (i <= 0) (entry -> "")
10.5 else (entry.substring(0, i) -> entry.substring(i + 1))
10.6 }
10.7 - Map(entries: _*) +
10.8 - ("HOME" -> System.getenv("HOME")) +
10.9 - ("PATH" -> System.getenv("PATH"))
10.10 + Map(entries: _*) + ("PATH" -> System.getenv("PATH"))
10.11 }
10.12 }
10.13 _state = Some(State(standard_system, settings))
10.14 @@ -91,8 +89,7 @@
10.15
10.16 /* getenv */
10.17
10.18 - def getenv(name: String): String =
10.19 - settings.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
10.20 + def getenv(name: String): String = settings.getOrElse(name, "")
10.21
10.22 def getenv_strict(name: String): String =
10.23 {