--- a/NEWS Wed Jun 27 11:16:43 2018 +0200
+++ b/NEWS Wed Jun 27 20:31:22 2018 +0200
@@ -474,10 +474,16 @@
* The command-line tool "isabelle mkroot -I" initializes a Mercurial
repository for the generated session files.
+* Settings ISABELLE_HEAPS + ISABELLE_BROWSER_INFO (or
+ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build
+mode") determine the directory locations of the main build artefacts --
+instead of hard-wired directories in ISABELLE_HOME_USER (or
+ISABELLE_HOME).
+
* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
heap images and session databases are always stored in
-$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
-$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
+$ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or
+$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER (main Isabelle application or
"isabelle jedit -s" or "isabelle build -s").
* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
--- a/etc/settings Wed Jun 27 11:16:43 2018 +0200
+++ b/etc/settings Wed Jun 27 20:31:22 2018 +0200
@@ -77,8 +77,13 @@
# Location for temporary files (should be on a local file system).
ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER"
+# Heap locations.
+ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps"
+ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps"
+
# HTML browser info.
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
+ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info"
# Site settings check -- just to make it a little bit harder to copy this file verbatim!
[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
--- a/src/Doc/System/Environment.thy Wed Jun 27 11:16:43 2018 +0200
+++ b/src/Doc/System/Environment.thy Wed Jun 27 20:31:22 2018 +0200
@@ -175,9 +175,17 @@
always the (native) 64 bit variant: \<^verbatim>\<open>x86_64-linux\<close>, \<^verbatim>\<open>x86_64-darwin\<close>,
\<^verbatim>\<open>x86_64-windows\<close>.
- \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
- browser information is stored as HTML and PDF (see also \secref{sec:info}).
- The default value is @{path "$ISABELLE_HOME_USER/browser_info"}.
+ \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where HTML and PDF
+ browser information is stored (see also \secref{sec:info}); its default is
+ @{path "$ISABELLE_HOME_USER/browser_info"}. For ``system build mode'' (see
+ \secref{sec:tool-build}), @{setting_def ISABELLE_BROWSER_INFO_SYSTEM} is
+ used instead; its default is @{path "$ISABELLE_HOME/browser_info"}.
+
+ \<^descr>[@{setting_def ISABELLE_HEAPS}] is the directory where session heap images,
+ log files, and build databases are stored; its default is @{path
+ "$ISABELLE_HOME_USER/heaps"}. For ``system build mode'' (see
+ \secref{sec:tool-build}), @{setting_def ISABELLE_HEAPS_SYSTEM} is used
+ instead; its default is @{path "$ISABELLE_HOME/heaps"}.
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
--- a/src/Doc/System/Server.thy Wed Jun 27 11:16:43 2018 +0200
+++ b/src/Doc/System/Server.thy Wed Jun 27 20:31:22 2018 +0200
@@ -708,9 +708,9 @@
in a robust manner, instead of relying on directory locations.
\<^medskip>
- The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
- log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
- @{path "$ISABELLE_HOME_USER/heaps"}. See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
+ If \<open>system_mode\<close> is \<^verbatim>\<open>true\<close>, session images are stored in @{path
+ "$ISABELLE_HEAPS_SYSTEM"} instead of @{path "$ISABELLE_HEAPS"}. See also
+ option \<^verbatim>\<open>-s\<close> in @{tool build} (\secref{sec:tool-build}).
\<^medskip>
The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
--- a/src/Doc/System/Sessions.thy Wed Jun 27 11:16:43 2018 +0200
+++ b/src/Doc/System/Sessions.thy Wed Jun 27 20:31:22 2018 +0200
@@ -395,9 +395,9 @@
performance tuning on Linux servers with separate CPU/memory modules.
\<^medskip>
- Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images
- and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the
- default location @{path "$ISABELLE_HOME_USER/heaps"}.
+ Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that session images are
+ stored in @{path "$ISABELLE_HEAPS_SYSTEM"} instead of @{path
+ "$ISABELLE_HEAPS"}.
\<^medskip>
Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
--- a/src/Pure/Thy/sessions.scala Wed Jun 27 11:16:43 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Wed Jun 27 20:31:22 2018 +0200
@@ -1012,8 +1012,8 @@
/* directories */
- val system_output_dir: Path = Path.explode("~~/heaps/$ML_IDENTIFIER")
- val user_output_dir: Path = Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")
+ val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
+ val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
val output_dir: Path =
if (system_mode) system_output_dir else user_output_dir
@@ -1023,7 +1023,7 @@
else List(user_output_dir, system_output_dir)
val browser_info: Path =
- if (system_mode) Path.explode("~~/browser_info")
+ if (system_mode) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
else Path.explode("$ISABELLE_BROWSER_INFO")