1.1 --- a/NEWS Sun Nov 30 12:25:54 2008 +0100
1.2 +++ b/NEWS Sun Nov 30 12:58:20 2008 +0100
1.3 @@ -31,6 +31,16 @@
1.4 purge installed copies of Isabelle executables and re-run "isabelle
1.5 install -p ...", or use symlinks.
1.6
1.7 +* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
1.8 +old ~/isabelle, which was slightly non-standard and apt cause
1.9 +surprises on case-insensitive file-systems.
1.10 +
1.11 +INCOMPATIBILITY, need to move existing ~/isabelle/etc,
1.12 +~/isabelle/heaps, ~/isabelle/browser_info to the new place. Special
1.13 +care is required when using older releases of Isabelle. Note that
1.14 +ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any
1.15 +Isabelle distribution.
1.16 +
1.17 * The Isabelle System Manual (system) has been updated, with formally
1.18 checked references as hyperlinks.
1.19
2.1 --- a/doc-src/System/Thy/Basics.thy Sun Nov 30 12:25:54 2008 +0100
2.2 +++ b/doc-src/System/Thy/Basics.thy Sun Nov 30 12:58:20 2008 +0100
2.3 @@ -100,7 +100,7 @@
2.4 \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
2.5 exists) is run in the same way as the site default settings. Note
2.6 that the variable @{setting ISABELLE_HOME_USER} has already been set
2.7 - before --- usually to @{verbatim "~/isabelle"}.
2.8 + before --- usually to @{verbatim "~/.isabelle"}.
2.9
2.10 Thus individual users may override the site-wide defaults. See also
2.11 file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the
2.12 @@ -161,7 +161,7 @@
2.13
2.14 \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
2.15 counterpart of @{setting ISABELLE_HOME}. The default value is
2.16 - @{verbatim "~/isabelle"}, under rare circumstances this may be
2.17 + @{verbatim "~/.isabelle"}, under rare circumstances this may be
2.18 changed in the global setting file. Typically, the @{setting
2.19 ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
2.20 some extend. In particular, site-wide defaults may be overridden by
3.1 --- a/doc-src/System/Thy/Presentation.thy Sun Nov 30 12:25:54 2008 +0100
3.2 +++ b/doc-src/System/Thy/Presentation.thy Sun Nov 30 12:58:20 2008 +0100
3.3 @@ -93,7 +93,7 @@
3.4 @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool
3.5 make}~@{verbatim all}. The presentation output will appear in
3.6 @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
3.7 - @{verbatim "~/isabelle/browser_info/FOL"}. Note that option
3.8 + @{verbatim "~/.isabelle/browser_info/FOL"}. Note that option
3.9 @{verbatim "-v true"} will make the internal runs of @{tool usedir}
3.10 more explicit about such details.
3.11
3.12 @@ -756,7 +756,7 @@
3.13 This enables users to inspect {\LaTeX} runs in further detail, e.g.\
3.14 like this:
3.15 \begin{ttbox}
3.16 - cd ~/isabelle/browser_info/HOL/Test/document
3.17 + cd ~/.isabelle/browser_info/HOL/Test/document
3.18 isabelle latex -o pdf
3.19 \end{ttbox}
3.20 *}
4.1 --- a/doc-src/System/Thy/document/Basics.tex Sun Nov 30 12:25:54 2008 +0100
4.2 +++ b/doc-src/System/Thy/document/Basics.tex Sun Nov 30 12:58:20 2008 +0100
4.3 @@ -117,7 +117,7 @@
4.4 \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
4.5 exists) is run in the same way as the site default settings. Note
4.6 that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set
4.7 - before --- usually to \verb|~/isabelle|.
4.8 + before --- usually to \verb|~/.isabelle|.
4.9
4.10 Thus individual users may override the site-wide defaults. See also
4.11 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
4.12 @@ -178,7 +178,7 @@
4.13
4.14 \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
4.15 counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is
4.16 - \verb|~/isabelle|, under rare circumstances this may be
4.17 + \verb|~/.isabelle|, under rare circumstances this may be
4.18 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
4.19 some extend. In particular, site-wide defaults may be overridden by
4.20 a private \verb|$ISABELLE_HOME_USER/etc/settings|.
5.1 --- a/doc-src/System/Thy/document/Presentation.tex Sun Nov 30 12:25:54 2008 +0100
5.2 +++ b/doc-src/System/Thy/document/Presentation.tex Sun Nov 30 12:58:20 2008 +0100
5.3 @@ -108,7 +108,7 @@
5.4 and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
5.5 \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
5.6 \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
5.7 - \verb|~/isabelle/browser_info/FOL|. Note that option
5.8 + \verb|~/.isabelle/browser_info/FOL|. Note that option
5.9 \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
5.10 more explicit about such details.
5.11
5.12 @@ -764,7 +764,7 @@
5.13 This enables users to inspect {\LaTeX} runs in further detail, e.g.\
5.14 like this:
5.15 \begin{ttbox}
5.16 - cd ~/isabelle/browser_info/HOL/Test/document
5.17 + cd ~/.isabelle/browser_info/HOL/Test/document
5.18 isabelle latex -o pdf
5.19 \end{ttbox}%
5.20 \end{isamarkuptext}%
6.1 --- a/doc-src/TutorialI/Documents/Documents.thy Sun Nov 30 12:25:54 2008 +0100
6.2 +++ b/doc-src/TutorialI/Documents/Documents.thy Sun Nov 30 12:58:20 2008 +0100
6.3 @@ -344,7 +344,7 @@
6.4 session is derived from a single parent, usually an object-logic
6.5 image like \texttt{HOL}. This results in an overall tree structure,
6.6 which is reflected by the output location in the file system
6.7 - (usually rooted at \verb,~/isabelle/browser_info,).
6.8 + (usually rooted at \verb,~/.isabelle/browser_info,).
6.9
6.10 \medskip The easiest way to manage Isabelle sessions is via
6.11 \texttt{isabelle mkdir} (generates an initial session source setup)
7.1 --- a/etc/settings Sun Nov 30 12:25:54 2008 +0100
7.2 +++ b/etc/settings Sun Nov 30 12:58:20 2008 +0100
7.3 @@ -128,7 +128,7 @@
7.4 ###
7.5
7.6 # The place for user configuration, heap files, etc.
7.7 -ISABELLE_HOME_USER=~/isabelle
7.8 +ISABELLE_HOME_USER=~/.isabelle
7.9
7.10 # Where to look for isabelle tools (multiple dirs separated by ':').
7.11 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
8.1 --- a/etc/user-settings.sample Sun Nov 30 12:25:54 2008 +0100
8.2 +++ b/etc/user-settings.sample Sun Nov 30 12:58:20 2008 +0100
8.3 @@ -1,7 +1,7 @@
8.4 # -*- shell-script -*-
8.5 # $Id$
8.6 #
8.7 -# Isabelle user settings sample -- for use in ~/isabelle/etc/settings
8.8 +# Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
8.9
8.10 ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
8.11 HOL_USEDIR_OPTIONS="-p 1"