# HG changeset patch
# User wenzelm
# Date 1526737545 -7200
# Node ID c0341c0080e24e18591766d6eef7dd3096502702
# Parent  92050155593ed68e7ae026fe4092eff68c1d682c
clarified store directories;
discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT;

diff -r 92050155593e -r c0341c0080e2 NEWS
--- a/NEWS	Sat May 19 14:52:01 2018 +0200
+++ b/NEWS	Sat May 19 15:45:45 2018 +0200
@@ -351,6 +351,12 @@
 
 *** System ***
 
+* 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 jedit -s" or "isabelle build -s").
+
 * The command-line tool retrieves theory exports from the session build
 database.
 
diff -r 92050155593e -r c0341c0080e2 etc/settings
--- a/etc/settings	Sat May 19 14:52:01 2018 +0200
+++ b/etc/settings	Sat May 19 15:45:45 2018 +0200
@@ -77,11 +77,7 @@
 # Location for temporary files (should be on a local file system).
 ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER"
 
-# Heap input locations. ML system identifier is included in lookup.
-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"
+# HTML browser info.
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
 # Site settings check -- just to make it a little bit harder to copy this file verbatim!
diff -r 92050155593e -r c0341c0080e2 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sat May 19 14:52:01 2018 +0200
+++ b/lib/scripts/getsettings	Sat May 19 15:45:45 2018 +0200
@@ -99,8 +99,6 @@
   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
 fi
 
-ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
-
 #enforce JAVA_HOME
 if [ -d "$ISABELLE_JDK_HOME/jre" ]
 then
diff -r 92050155593e -r c0341c0080e2 src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Sat May 19 14:52:01 2018 +0200
+++ b/src/Doc/System/Environment.thy	Sat May 19 15:45:45 2018 +0200
@@ -73,14 +73,9 @@
   minimum.
 
   \<^medskip>
-  A few variables are somewhat special:
-
-    \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
-    name of the @{executable isabelle} executables.
-
-    \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
-    distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
-    @{setting ML_IDENTIFIER}) appended automatically to its value.
+  A few variables are somewhat special, e.g. @{setting_def ISABELLE_TOOL} is
+  set automatically to the absolute path name of the @{executable isabelle}
+  executables.
 
   \<^medskip>
   Note that the settings environment may be inspected with the @{tool getenv}
@@ -180,15 +175,6 @@
   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_PATH}] is a list of directories (separated by
-  colons) where Isabelle logic images may reside. When looking up heaps files,
-  the value of @{setting ML_IDENTIFIER} is appended to each component
-  internally.
-
-  \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
-  should be stored by default. The ML system and Isabelle version identifier
-  is appended here, too.
-
   \<^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"}.
diff -r 92050155593e -r c0341c0080e2 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sat May 19 14:52:01 2018 +0200
+++ b/src/Doc/System/Misc.thy	Sat May 19 15:45:45 2018 +0200
@@ -145,7 +145,7 @@
   \<^medskip>
   Get the value only of the same settings variable, which is particularly
   useful in shell scripts:
-  @{verbatim [display] \<open>isabelle getenv -b ISABELLE_OUTPUT\<close>}
+  @{verbatim [display] \<open>isabelle getenv -b ISABELLE_HOME_USER\<close>}
 \<close>
 
 
diff -r 92050155593e -r c0341c0080e2 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat May 19 14:52:01 2018 +0200
+++ b/src/Doc/System/Server.thy	Sat May 19 15:45:45 2018 +0200
@@ -709,8 +709,7 @@
   \<^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
-  @{setting ISABELLE_OUTPUT} (which is normally in @{setting
-  ISABELLE_HOME_USER}). See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
+  @{path "$ISABELLE_HOME_USER/heaps"}. See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
 
   \<^medskip>
   The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
diff -r 92050155593e -r c0341c0080e2 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat May 19 14:52:01 2018 +0200
+++ b/src/Doc/System/Sessions.thy	Sat May 19 15:45:45 2018 +0200
@@ -391,8 +391,7 @@
   \<^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 @{setting ISABELLE_OUTPUT} (which is normally in @{setting
-  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
+  default location @{path "$ISABELLE_HOME_USER/heaps"}.
 
   \<^medskip>
   Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
diff -r 92050155593e -r c0341c0080e2 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat May 19 14:52:01 2018 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat May 19 15:45:45 2018 +0200
@@ -190,7 +190,9 @@
       val ml_platform =
         augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
 
-      val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
+      val isabelle_output =
+        other_isabelle.isabelle_home_user + Path.explode("heaps") +
+          Path.explode(other_isabelle("getenv -b ML_IDENTIFIER").check.out)
       val isabelle_output_log = isabelle_output + Path.explode("log")
       val isabelle_base_log = isabelle_output + Path.explode("../base_log")
 
diff -r 92050155593e -r c0341c0080e2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat May 19 14:52:01 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat May 19 15:45:45 2018 +0200
@@ -966,6 +966,9 @@
 
   class Store private[Sessions](val options: Options, val system_mode: Boolean)
   {
+    override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
+
+
     /* file names */
 
     def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
@@ -973,19 +976,26 @@
     def log_gz(name: String): Path = log(name).ext("gz")
 
 
-    /* output */
+    /* directories */
+
+    def system_output_dir: Path = Path.explode("~~/heaps/$ML_IDENTIFIER")
+    def user_output_dir: Path = Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")
+
+    def output_dir: Path =
+      if (system_mode) system_output_dir else user_output_dir
+
+    def input_dirs: List[Path] =
+      if (system_mode) List(system_output_dir)
+      else List(user_output_dir, system_output_dir)
 
     val browser_info: Path =
       if (system_mode) Path.explode("~~/browser_info")
       else Path.explode("$ISABELLE_BROWSER_INFO")
 
-    val output_dir: Path =
-      if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
-      else Path.explode("$ISABELLE_OUTPUT")
 
-    override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
+    /* output */
 
-    def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
+    def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
 
     def output_heap(name: String): Path = output_dir + Path.basic(name)
     def output_log(name: String): Path = output_dir + log(name)
@@ -997,13 +1007,6 @@
 
     /* input */
 
-    private val input_dirs =
-      if (system_mode) List(output_dir)
-      else {
-        val ml_ident = Path.explode("$ML_IDENTIFIER").expand
-        output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
-      }
-
     def find_heap(name: String): Option[Path] =
       input_dirs.map(_ + Path.basic(name)).find(_.is_file)
 
diff -r 92050155593e -r c0341c0080e2 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat May 19 14:52:01 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sat May 19 15:45:45 2018 +0200
@@ -465,7 +465,7 @@
 
     val queue = Queue(progress, deps.sessions_structure, store)
 
-    store.prepare_output()
+    store.prepare_output_dir()
 
     // cleanup
     def cleanup(name: String, echo: Boolean = false)