USER_HOME settings variable points to cross-platform user home directory;
authorwenzelm
Sun Apr 22 14:30:18 2012 +0200 (2012-04-22)
changeset 47661012a887997f3
parent 47660 7a5c681c0265
child 47662 206bf8c4860d
USER_HOME settings variable points to cross-platform user home directory;
NEWS
doc-src/IsarRef/Thy/Misc.thy
doc-src/IsarRef/Thy/document/Misc.tex
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/document/Basics.tex
etc/settings
lib/scripts/getsettings
src/Pure/General/path.ML
src/Pure/General/path.scala
src/Pure/System/isabelle_system.scala
     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    {