# HG changeset patch
# User wenzelm
# Date 1749904314 -7200
# Node ID e9b9af6da795dcb3033671241d1b1ded07789e51
# Parent  e0fb460181876c6ec97afcff7a3312d277d53d64
clarified signature;

diff -r e0fb46018187 -r e9b9af6da795 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -128,7 +128,7 @@
             Store.Sources.load(session_background.base, cache = store.cache.compress)
 
           val env =
-            Isabelle_System.settings(
+            Isabelle_System.Settings.env(
               List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString))
 
           val session_heaps =
diff -r e0fb46018187 -r e9b9af6da795 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Pure/General/path.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -315,7 +315,7 @@
     new Path(Path.norm_elems(elems.flatMap(eval)))
   }
 
-  def expand: Path = expand_env(Isabelle_System.settings_env())
+  def expand: Path = expand_env(Isabelle_System.Settings())
 
   def file_name: String = expand.base.implode
 
diff -r e0fb46018187 -r e9b9af6da795 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Pure/General/ssh.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -556,7 +556,7 @@
         cleanup: () => Unit = () => ()
     ): Bash.Process = {
       Bash.process(script, description = description, cwd = cwd, redirect = redirect,
-        env = if (settings) Isabelle_System.settings() else null,
+        env = if (settings) Isabelle_System.Settings.env() else null,
         cleanup = cleanup)
     }
 
diff -r e0fb46018187 -r e9b9af6da795 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Pure/ML/ml_process.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -36,7 +36,7 @@
     args: List[String] = Nil,
     modes: List[String] = Nil,
     cwd: Path = Path.current,
-    env: JMap[String, String] = Isabelle_System.settings(),
+    env: JMap[String, String] = Isabelle_System.Settings.env(),
     redirect: Boolean = false,
     cleanup: () => Unit = () => ()
   ): Bash.Process = {
diff -r e0fb46018187 -r e9b9af6da795 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Pure/System/bash.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -91,7 +91,7 @@
       description: String = "",
       ssh: SSH.System = SSH.Local,
       cwd: Path = Path.current,
-      env: JMap[String, String] = Isabelle_System.settings(),  // ignored for remote ssh
+      env: JMap[String, String] = Isabelle_System.Settings.env(),  // ignored for remote ssh
       redirect: Boolean = false,
       cleanup: () => Unit = () => ()): Process =
     new Process(script, description, ssh, cwd, env, redirect, cleanup)
@@ -376,7 +376,7 @@
                   case Some(s) => Path.explode(s)
                 },
               env =
-                Isabelle_System.settings(
+                Isabelle_System.Settings.env(
                   XML.Decode.list(XML.Decode.pair(XML.Decode.string, XML.Decode.string))(
                     YXML.parse_body(YXML.Source(putenv)))),
               redirect = redirect)
diff -r e0fb46018187 -r e9b9af6da795 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -20,7 +20,7 @@
     eval_main: String = "",
     modes: List[String] = Nil,
     cwd: Path = Path.current,
-    env: JMap[String, String] = Isabelle_System.settings()
+    env: JMap[String, String] = Isabelle_System.Settings.env()
   ): Isabelle_Process = {
     val channel = System_Channel()
     val process =
diff -r e0fb46018187 -r e9b9af6da795 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -30,22 +30,24 @@
 
   object No_Env extends Env(JMap.of())
 
-  def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = {
-    val env0 = isabelle.setup.Environment.settings()
-    if (putenv.isEmpty) env0
-    else {
-      val env = new HashMap(env0)
-      for ((a, b) <- putenv) env.put(a, b)
-      env
+  object Settings {
+    def env(putenv: List[(String, String)] = Nil): JMap[String, String] = {
+      val env0 = isabelle.setup.Environment.settings()
+      if (putenv.isEmpty) env0
+      else {
+        val env = new HashMap(env0)
+        for ((a, b) <- putenv) env.put(a, b)
+        env
+      }
     }
+
+    def apply(putenv: List[(String, String)] = Nil): Settings_Env =
+      new Env(env(putenv = putenv))
   }
 
-  def settings_env(putenv: List[(String, String)] = Nil): Settings_Env =
-    new Env(settings(putenv = putenv))
+  def getenv(name: String, env: Settings = Settings()): String = env.get(name)
 
-  def getenv(name: String, env: Settings = settings_env()): String = env.get(name)
-
-  def getenv_strict(name: String, env: Settings = settings_env()): String =
+  def getenv_strict(name: String, env: Settings = Settings()): String =
     proper_string(getenv(name, env)) getOrElse
       error("Undefined Isabelle environment variable: " + quote(name))
 
@@ -413,7 +415,7 @@
     description: String = "",
     ssh: SSH.System = SSH.Local,
     cwd: Path = Path.current,
-    env: JMap[String, String] = settings(),  // ignored for remote ssh
+    env: JMap[String, String] = Settings.env(),  // ignored for remote ssh
     redirect: Boolean = false,
     input: String = "",
     progress_stdout: String => Unit = (_: String) => (),
diff -r e0fb46018187 -r e9b9af6da795 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Pure/System/progress.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -95,7 +95,7 @@
   final def bash(script: String,
     ssh: SSH.System = SSH.Local,
     cwd: Path = Path.current,
-    env: JMap[String, String] = Isabelle_System.settings(),  // ignored for remote ssh
+    env: JMap[String, String] = Isabelle_System.Settings.env(),  // ignored for remote ssh
     redirect: Boolean = false,
     echo: Boolean = false,
     watchdog_time: Time = Time.zero,
diff -r e0fb46018187 -r e9b9af6da795 src/Pure/Tools/profiling.scala
--- a/src/Pure/Tools/profiling.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Pure/Tools/profiling.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -87,7 +87,7 @@
           val session_heaps =
             ML_Process.session_heaps(store, session_background, logic = session_name)
           ML_Process(store.options, session_background, session_heaps, args = eval_args,
-            env = Isabelle_System.settings(put_env)).result().check
+            env = Isabelle_System.Settings.env(put_env)).result().check
           decode_result(YXML.parse_body(Bytes.read(dir + Path.explode("result.yxml"))))
         }
       }
diff -r e0fb46018187 -r e9b9af6da795 src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Sat Jun 14 11:45:56 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_main.scala	Sat Jun 14 14:31:54 2025 +0200
@@ -50,7 +50,7 @@
       JSON.optional("verbose" -> proper_bool(verbose))
 
     val env =
-      Isabelle_System.settings(environment ::: List(
+      Isabelle_System.Settings.env(environment ::: List(
         "ISABELLE_VSCODIUM_ARGS" -> JSON.Format(args_json),
         "ISABELLE_VSCODIUM_APP" -> platform_path("$ISABELLE_VSCODIUM_RESOURCES/vscodium"),
         "ELECTRON_RUN_AS_NODE" -> "1"))