# HG changeset patch
# User wenzelm
# Date 1288995560 -3600
# Node ID e4c9e0dad473dc2671ab43fda04ead39fb48388f
# Parent  bdce9a9ec0cd7ba3dce1bff98d67f91f1b168d9f
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;

diff -r bdce9a9ec0cd -r e4c9e0dad473 NEWS
--- a/NEWS	Fri Nov 05 22:03:57 2010 +0100
+++ b/NEWS	Fri Nov 05 23:19:20 2010 +0100
@@ -6,6 +6,13 @@
 
 *** General ***
 
+* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
+(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
+while the default heap location within that directory lacks that extra
+suffix.  This isolates multiple Isabelle installations from each
+other, avoiding problems with old settings in new versions.
+INCOMPATIBILITY, need to copy/upgrade old user settings manually.
+
 * Significantly improved Isabelle/Isar implementation manual.
 
 * Explicit treatment of UTF8 sequences as Isabelle symbols, such that
diff -r bdce9a9ec0cd -r e4c9e0dad473 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Fri Nov 05 22:03:57 2010 +0100
+++ b/doc-src/System/Thy/Basics.thy	Fri Nov 05 23:19:20 2010 +0100
@@ -95,7 +95,8 @@
   \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
   exists) is run in the same way as the site default settings. Note
   that the variable @{setting ISABELLE_HOME_USER} has already been set
-  before --- usually to @{verbatim "~/.isabelle"}.
+  before --- usually to something like @{verbatim
+  "$HOME/.isabelle/IsabelleXXXX"}.
   
   Thus individual users may override the site-wide defaults.  See also
   file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the
@@ -156,11 +157,12 @@
   
   \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
   counterpart of @{setting ISABELLE_HOME}. The default value is
-  @{verbatim "~/.isabelle"}, under rare circumstances this may be
-  changed in the global setting file.  Typically, the @{setting
-  ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
-  some extend. In particular, site-wide defaults may be overridden by
-  a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
+  relative to @{verbatim "$HOME/.isabelle"}, under rare circumstances
+  this may be changed in the global setting file.  Typically, the
+  @{setting ISABELLE_HOME_USER} directory mimics @{setting
+  ISABELLE_HOME} to some extend. In particular, site-wide defaults may
+  be overridden by a private @{verbatim
+  "$ISABELLE_HOME_USER/etc/settings"}.
   
   \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
   set to a symbolic identifier for the underlying hardware and
diff -r bdce9a9ec0cd -r e4c9e0dad473 doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Fri Nov 05 22:03:57 2010 +0100
+++ b/doc-src/System/Thy/Presentation.thy	Fri Nov 05 23:19:20 2010 +0100
@@ -88,10 +88,11 @@
 \end{ttbox}
 
   and then change into the @{"file" "~~/src/FOL"} directory and run
-  @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool
-  make}~@{verbatim all}.  The presentation output will appear in
-  @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
-  @{verbatim "~/.isabelle/browser_info/FOL"}.  Note that option
+  @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle}
+  @{tool make}~@{verbatim all}.  The presentation output will appear
+  in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
+  something like @{verbatim
+  "~/.isabelle/IsabelleXXXX/browser_info/FOL"}.  Note that option
   @{verbatim "-v true"} will make the internal runs of @{tool usedir}
   more explicit about such details.
 
@@ -768,7 +769,7 @@
   This enables users to inspect {\LaTeX} runs in further detail, e.g.\
   like this:
 \begin{ttbox}
-  cd ~/.isabelle/browser_info/HOL/Test/document
+  cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
   isabelle latex -o pdf
 \end{ttbox}
 *}
diff -r bdce9a9ec0cd -r e4c9e0dad473 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Fri Nov 05 22:03:57 2010 +0100
+++ b/doc-src/System/Thy/document/Basics.tex	Fri Nov 05 23:19:20 2010 +0100
@@ -114,7 +114,7 @@
   \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
   exists) is run in the same way as the site default settings. Note
   that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set
-  before --- usually to \verb|~/.isabelle|.
+  before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
   
   Thus individual users may override the site-wide defaults.  See also
   file \hyperlink{file.$ISABELLE-HOME/etc/user-settings.sample}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}user{\isacharminus}settings{\isachardot}sample}}}} in the
@@ -175,10 +175,10 @@
   
   \item[\indexdef{}{setting}{ISABELLE\_HOME\_USER}\hypertarget{setting.ISABELLE-HOME-USER}{\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}}}] is the user-specific
   counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is
-  \verb|~/.isabelle|, under rare circumstances this may be
-  changed in the global setting file.  Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to
-  some extend. In particular, site-wide defaults may be overridden by
-  a private \verb|$ISABELLE_HOME_USER/etc/settings|.
+  relative to \verb|$HOME/.isabelle|, under rare circumstances
+  this may be changed in the global setting file.  Typically, the
+  \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to some extend. In particular, site-wide defaults may
+  be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
   
   \item[\indexdef{}{setting}{ISABELLE\_PLATFORM}\hypertarget{setting.ISABELLE-PLATFORM}{\hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is automatically
   set to a symbolic identifier for the underlying hardware and
diff -r bdce9a9ec0cd -r e4c9e0dad473 doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex	Fri Nov 05 22:03:57 2010 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex	Fri Nov 05 23:19:20 2010 +0100
@@ -104,9 +104,10 @@
 \end{ttbox}
 
   and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
-  \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|.  The presentation output will appear in
-  \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
-  \verb|~/.isabelle/browser_info/FOL|.  Note that option
+  \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle|
+  \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|.  The presentation output will appear
+  in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
+  something like \verb|~/.isabelle/IsabelleXXXX/browser_info/FOL|.  Note that option
   \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
   more explicit about such details.
 
@@ -776,7 +777,7 @@
   This enables users to inspect {\LaTeX} runs in further detail, e.g.\
   like this:
 \begin{ttbox}
-  cd ~/.isabelle/browser_info/HOL/Test/document
+  cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
   isabelle latex -o pdf
 \end{ttbox}%
 \end{isamarkuptext}%
diff -r bdce9a9ec0cd -r e4c9e0dad473 etc/settings
--- a/etc/settings	Fri Nov 05 22:03:57 2010 +0100
+++ b/etc/settings	Fri Nov 05 23:19:20 2010 +0100
@@ -103,7 +103,7 @@
 ###
 
 # The place for user configuration, heap files, etc.
-ISABELLE_HOME_USER=~/.isabelle
+ISABELLE_HOME_USER="$HOME/.isabelle/$ISABELLE_IDENTIFIER"
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
@@ -112,10 +112,10 @@
 ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
 
 # Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
 
 # Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER"
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
 # Site settings check -- just to make it a little bit harder to copy this file verbatim!