more uniform signature for various process invocations;
env refers to full environment, not the update;
--- a/src/Pure/System/bash.scala Sun Mar 13 11:48:38 2016 +0100
+++ b/src/Pure/System/bash.scala Sun Mar 13 12:37:01 2016 +0100
@@ -28,7 +28,7 @@
def process(script: String,
cwd: JFile = null,
- env: Map[String, String] = Map.empty,
+ env: Map[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => ()): Process =
new Process(script, cwd, env, redirect, cleanup)
@@ -48,9 +48,10 @@
File.write(script_file, script)
private val proc =
- Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
- File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
- File.standard_path(timing_file), "bash", File.standard_path(script_file))
+ Isabelle_System.process(
+ List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
+ File.standard_path(timing_file), "bash", File.standard_path(script_file)),
+ cwd = cwd, env = env, redirect = redirect)
// channels
--- a/src/Pure/System/cygwin.scala Sun Mar 13 11:48:38 2016 +0100
+++ b/src/Pure/System/cygwin.scala Sun Mar 13 12:37:01 2016 +0100
@@ -21,11 +21,11 @@
{
require(Platform.is_windows)
- def execute(args: String*)
+ def exec(cmdline: String*)
{
val cwd = new JFile(isabelle_root)
- val env = Map("CYGWIN" -> "nodosfilewarning")
- val proc = Isabelle_System.process(cwd, env, true, args: _*)
+ val env = sys.env + ("CYGWIN" -> "nodosfilewarning")
+ val proc = Isabelle_System.process(cmdline.toList, cwd = cwd, env = env, redirect = true)
val (output, rc) = Isabelle_System.process_output(proc)
if (rc != 0) error(output)
}
@@ -58,8 +58,8 @@
}
recover_symlinks(symlinks)
- execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
- execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
+ exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
+ exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
}
}
}
--- a/src/Pure/System/isabelle_system.scala Sun Mar 13 11:48:38 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala Sun Mar 13 12:37:01 2016 +0100
@@ -51,10 +51,10 @@
@volatile private var _settings: Option[Map[String, String]] = None
- def settings(env: Map[String, String] = Map.empty): Map[String, String] =
+ def settings(): Map[String, String] =
{
if (_settings.isEmpty) init() // unsynchronized check
- if (env == null) _settings.get else _settings.get ++ env
+ _settings.get
}
def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
@@ -112,11 +112,11 @@
List(isabelle_root1 + JFile.separator + "bin" + JFile.separator + "isabelle",
"getenv", "-d", dump.toString)
- val (output, rc) = process_output(process(null, env, true, (cmd1 ::: cmd2): _*))
+ val (output, rc) = process_output(process(cmd1 ::: cmd2, env = env, redirect = true))
if (rc != 0) error(output)
val entries =
- (for (entry <- File.read(dump) split "\u0000" if entry != "") yield {
+ (for (entry <- File.read(dump).split("\u0000") if entry != "") yield {
val i = entry.indexOf('=')
if (i <= 0) entry -> ""
else entry.substring(0, i) -> entry.substring(i + 1)
@@ -177,10 +177,13 @@
/* raw process */
- def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
+ def process(command_line: List[String],
+ cwd: JFile = null,
+ env: Map[String, String] = settings(),
+ redirect: Boolean = false): Process =
{
val cmdline = new java.util.LinkedList[String]
- for (s <- args) cmdline.add(s)
+ for (s <- command_line) cmdline.add(s)
val proc = new ProcessBuilder(cmdline)
if (cwd != null) proc.directory(cwd)
@@ -211,17 +214,15 @@
/* plain execute */
- def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
+ def execute(command_line: List[String],
+ cwd: JFile = null, env: Map[String, String] = null, redirect: Boolean = false): Process =
{
- val cmdline =
- if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ::: args.toList
- else args
- process(cwd, settings(env), redirect, cmdline: _*)
+ val command_line1 =
+ if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ::: command_line
+ else command_line
+ process(command_line1, cwd = cwd, env = env, redirect = redirect)
}
- def execute(redirect: Boolean, args: String*): Process =
- execute_env(null, null, redirect, args: _*)
-
/* tmp files */
@@ -295,21 +296,23 @@
val bash =
if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
- val cmdline = bash ::: List("-c", "kill -" + signal + " -" + group_pid)
- process_output(process(null, null, true, cmdline: _*))
+ process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
}
/* bash */
- def bash(script: String, cwd: JFile = null, env: Map[String, String] = Map.empty,
+ def bash(script: String,
+ cwd: JFile = null,
+ env: Map[String, String] = settings(),
+ redirect: Boolean = false,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
progress_limit: Option[Long] = None,
strict: Boolean = true,
cleanup: () => Unit = () => ()): Process_Result =
{
- Bash.process(script, cwd = cwd, env = env, cleanup = cleanup).
+ Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
result(progress_stdout, progress_stderr, progress_limit, strict)
}
@@ -328,7 +331,7 @@
} match {
case Some(dir) =>
val file = File.standard_path(dir + Path.basic(name))
- process_output(execute(true, (List(file) ::: args.toList): _*))
+ process_output(execute(file :: args.toList, redirect = true))
case None => ("Unknown Isabelle tool: " + name, 2)
}
}
--- a/src/Pure/Tools/build.scala Sun Mar 13 11:48:38 2016 +0100
+++ b/src/Pure/Tools/build.scala Sun Mar 13 12:37:01 2016 +0100
@@ -551,7 +551,9 @@
output.file.delete
- private val env = Map("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
+ private val env =
+ Isabelle_System.settings() +
+ ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
private val future_result: Future[Process_Result] =
Future.thread("build") {
@@ -582,8 +584,7 @@
ML_Process(info.options, parent,
List("--eval",
"Build.build " + ML_Syntax.print_string_raw(File.standard_path(args_file))),
- cwd = info.dir.file, env = env,
- cleanup = () => args_file.delete)
+ cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
}
process.result(
progress_stdout = (line: String) =>
--- a/src/Pure/Tools/ml_process.scala Sun Mar 13 11:48:38 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala Sun Mar 13 12:37:01 2016 +0100
@@ -18,7 +18,7 @@
modes: List[String] = Nil,
secure: Boolean = false,
cwd: JFile = null,
- env: Map[String, String] = Map.empty,
+ env: Map[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => (),
channel: Option[System_Channel] = None): Bash.Process =