--- 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 =
--- 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
--- 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)
}
--- 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 = {
--- 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)
--- 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 =
--- 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) => (),
--- 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,
--- 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"))))
}
}
--- 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"))