# HG changeset patch
# User wenzelm
# Date 1674586533 -3600
# Node ID 7e11e96a922d0f4ce825885e2ef4887e59f5d4dc
# Parent  395a0701a1255bfe6a33b945b73741e24488eac3
more formal Other_Isabelle.settings, with derived expand_path / bash_path;

diff -r 395a0701a125 -r 7e11e96a922d src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Jan 24 18:56:33 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Tue Jan 24 19:55:33 2023 +0100
@@ -197,8 +197,8 @@
       File.write(other_isabelle.etc_preferences, cat_lines(more_preferences))
 
       val isabelle_output =
-        other_isabelle.isabelle_home_user + Path.explode("heaps") +
-          Path.explode(other_isabelle.getenv("ML_IDENTIFIER"))
+        other_isabelle.expand_path(
+          Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER"))
       val isabelle_output_log = isabelle_output + Path.explode("log")
       val isabelle_base_log = isabelle_output + Path.explode("../base_log")
 
@@ -218,7 +218,7 @@
       Isabelle_System.rm_tree(isabelle_output)
       Isabelle_System.make_directory(isabelle_output)
 
-      (other_isabelle.isabelle_home_user + Path.explode("mash_state")).file.delete
+      other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/mash_state")).file.delete
 
       val log_path =
         other_isabelle.isabelle_home_user +
@@ -228,7 +228,7 @@
 
       Isabelle_System.make_directory(log_path.dir)
 
-      val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
+      val build_out = other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/log/build.out"))
       val build_out_progress = new File_Progress(build_out)
       build_out.file.delete
 
diff -r 395a0701a125 -r 7e11e96a922d src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Tue Jan 24 18:56:33 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Tue Jan 24 19:55:33 2023 +0100
@@ -46,11 +46,16 @@
   def getenv(name: String): String =
     bash("bin/isabelle getenv -b " + Bash.string(name)).check.out
 
-  val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
+  val settings: Isabelle_System.Settings = (name: String) => getenv(name)
+
+  def expand_path(path: Path): Path = path.expand_env(settings)
+  def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
 
-  val etc: Path = isabelle_home_user + Path.explode("etc")
-  val etc_settings: Path = etc + Path.explode("settings")
-  val etc_preferences: Path = etc + Path.explode("preferences")
+  def isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))
+
+  def etc: Path = expand_path(Path.explode("$ISABELLE_HOME_USER/etc"))
+  def etc_settings: Path = etc + Path.explode("settings")
+  def etc_preferences: Path = etc + Path.explode("preferences")
 
   def resolve_components(echo: Boolean = false): Unit = {
     val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING"))
@@ -65,14 +70,14 @@
       Isabelle_System.rm_tree(isabelle_home + Path.explode("lib/classes"))
     }
 
-    val dummy_stty = Path.explode("lib/dummy_stty/stty")
-    if (!(isabelle_home + dummy_stty).is_file) {
-      Isabelle_System.copy_file(Path.ISABELLE_HOME + dummy_stty,
-        Isabelle_System.make_directory(isabelle_home + dummy_stty.dir))
+    val dummy_stty = Path.explode("~~/lib/dummy_stty/stty")
+    if (!expand_path(dummy_stty).is_file) {
+      Isabelle_System.copy_file(dummy_stty,
+        Isabelle_System.make_directory(expand_path(dummy_stty.dir)))
     }
     try {
       bash(
-        "export PATH=\"" + File.bash_path(isabelle_home + dummy_stty.dir) + ":$PATH\"\n" +
+        "export PATH=\"" + bash_path(dummy_stty.dir) + ":$PATH\"\n" +
         "export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" +
         "bin/isabelle jedit -b", echo = echo).check
     }