# HG changeset patch
# User wenzelm
# Date 1674582993 -3600
# Node ID 395a0701a1255bfe6a33b945b73741e24488eac3
# Parent  a709945b6c7198b0ce5db70cbaadafa8f4d0a46d
clarified signature: minimal interface for getenv/expand_env, instead of bulky java.util.Map;

diff -r a709945b6c71 -r 395a0701a125 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Jan 24 18:26:20 2023 +0100
+++ b/src/Pure/General/path.scala	Tue Jan 24 18:56:33 2023 +0100
@@ -283,7 +283,7 @@
 
   /* expand */
 
-  def expand_env(env: JMap[String, String]): Path = {
+  def expand_env(env: Isabelle_System.Settings): Path = {
     def eval(elem: Path.Elem): List[Path.Elem] =
       elem match {
         case Path.Variable(s) =>
@@ -297,7 +297,7 @@
     new Path(Path.norm_elems(elems.flatMap(eval)))
   }
 
-  def expand: Path = expand_env(Isabelle_System.settings())
+  def expand: Path = expand_env(Isabelle_System.settings_env())
 
   def file_name: String = expand.base.implode
 
diff -r a709945b6c71 -r 395a0701a125 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Jan 24 18:26:20 2023 +0100
+++ b/src/Pure/General/ssh.scala	Tue Jan 24 18:56:33 2023 +0100
@@ -170,7 +170,8 @@
       }
     }
 
-    val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home)
+    val settings: Isabelle_System.Settings =
+      (name: String) => if (name == "HOME" || name == "USER_HOME") user_home else ""
 
     override def close(): Unit = {
       if (control_path.nonEmpty) run_ssh(opts = "-O exit").check
diff -r a709945b6c71 -r 395a0701a125 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Jan 24 18:26:20 2023 +0100
+++ b/src/Pure/System/isabelle_system.scala	Tue Jan 24 18:56:33 2023 +0100
@@ -21,6 +21,13 @@
 object Isabelle_System {
   /* settings environment */
 
+  trait Settings { def get(name: String): String }
+  trait Settings_Env extends Settings { def env: JMap[String, String] }
+
+  class Env(val env: JMap[String, String]) extends Settings_Env {
+    override def get(name: String): String = Option(env.get(name)).getOrElse("")
+  }
+
   def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = {
     val env0 = isabelle.setup.Environment.settings()
     if (putenv.isEmpty) env0
@@ -31,10 +38,12 @@
     }
   }
 
-  def getenv(name: String, env: JMap[String, String] = settings()): String =
-    Option(env.get(name)).getOrElse("")
+  def settings_env(putenv: List[(String, String)] = Nil): Settings_Env =
+    new Env(settings(putenv = putenv))
 
-  def getenv_strict(name: String, env: JMap[String, String] = settings()): String =
+  def getenv(name: String, env: Settings = settings_env()): String = env.get(name)
+
+  def getenv_strict(name: String, env: Settings = settings_env()): String =
     proper_string(getenv(name, env)) getOrElse
       error("Undefined Isabelle environment variable: " + quote(name))