# HG changeset patch
# User wenzelm
# Date 1510414095 -3600
# Node ID 897f1ac84aabb3ff3f8e6b91edb3fd9ec36bb2f4
# Parent  6c94f749410a2e5e732d314f96b35b3ac4c179a9
clarified settings environment;

diff -r 6c94f749410a -r 897f1ac84aab src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Sat Nov 11 16:01:02 2017 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Sat Nov 11 16:28:15 2017 +0100
@@ -10,18 +10,25 @@
 object Other_Isabelle
 {
   def apply(isabelle_home: Path,
-      isabelle_identifier: String,
+      isabelle_identifier: String = "",
+      user_home: Path = Path.explode("$USER_HOME"),
       progress: Progress = No_Progress): Other_Isabelle =
-    new Other_Isabelle(isabelle_home, isabelle_identifier, progress)
+    new Other_Isabelle(isabelle_home, isabelle_identifier, user_home, progress)
 }
 
 class Other_Isabelle(
   val isabelle_home: Path,
   val isabelle_identifier: String,
+  user_home: Path,
   progress: Progress)
 {
   other_isabelle =>
 
+  override def toString: String = isabelle_home.toString
+
+  if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
+    error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
+
 
   /* static system */
 
@@ -30,7 +37,9 @@
       redirect: Boolean = false,
       echo: Boolean = false,
       strict: Boolean = true): Process_Result =
-    progress.bash(Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
+    progress.bash(
+      "export USER_HOME=" + File.bash_path(user_home) + "\n" +
+      Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
       env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
 
   def apply(