--- a/src/Pure/Build/build_manager.scala Wed Apr 09 17:40:27 2025 +0200
+++ b/src/Pure/Build/build_manager.scala Wed Apr 09 22:23:59 2025 +0200
@@ -664,7 +664,7 @@
val log_opts = "--graph --color always"
val rev1 = "children(" + rev0 + ")"
val cmd = repository.command_line("log", Mercurial.opt_rev(rev1 + ":" + rev), log_opts)
- val log = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out
+ val log = Isabelle_System.bash(Bash.exports("HGPLAINEXCEPT=color") + cmd).check.out
if (log.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(log_ext).gz, log)
}
@@ -677,7 +677,7 @@
if (rev0.nonEmpty && rev.nonEmpty) {
val diff_opts = "--noprefix --nodates --ignore-all-space --color always"
val cmd = repository.command_line("diff", Mercurial.opt_rev(rev0 + ":" + rev), diff_opts)
- val diff = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out
+ val diff = Isabelle_System.bash(Bash.exports("HGPLAINEXCEPT=color") + cmd).check.out
if (diff.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(diff_ext).gz, diff)
}
--- a/src/Pure/General/mercurial.scala Wed Apr 09 17:40:27 2025 +0200
+++ b/src/Pure/General/mercurial.scala Wed Apr 09 22:23:59 2025 +0200
@@ -223,7 +223,8 @@
options: String = "",
repository: Boolean = true
): String = {
- "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
+ Bash.exports("LANG=C", "HGPLAIN=") +
+ "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
(if (repository) " --repository " + ssh.bash_path(root) else "") +
" --noninteractive " + name + " " + options + " " + args
}
--- a/src/Pure/ML/ml_statistics.scala Wed Apr 09 17:40:27 2025 +0200
+++ b/src/Pure/ML/ml_statistics.scala Wed Apr 09 22:23:59 2025 +0200
@@ -57,8 +57,7 @@
if (props.nonEmpty) consume(props)
}
- val env_prefix =
- if_proper(stats_dir, "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n")
+ val env_prefix = if_proper(stats_dir, Bash.exports("POLYSTATSDIR=" + stats_dir))
Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
--- a/src/Pure/System/bash.scala Wed Apr 09 17:40:27 2025 +0200
+++ b/src/Pure/System/bash.scala Wed Apr 09 22:23:59 2025 +0200
@@ -53,10 +53,8 @@
isabelle_identifier: String = "",
cwd: Path = Path.current
): String = {
- if_proper(user_home,
- "export USER_HOME=" + Bash.string(user_home) + "\n") +
- if_proper(isabelle_identifier,
- "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n") +
+ if_proper(user_home, exports("USER_HOME=" + user_home)) +
+ if_proper(isabelle_identifier, exports("ISABELLE_IDENTIFIER=" + isabelle_identifier)) +
(if (cwd == null || cwd.is_current) "" else "cd " + quote(cwd.implode) + "\n") +
script
}