# HG changeset patch
# User wenzelm
# Date 1457869021 -3600
# Node ID 4c89504c76fbea4ef57ff08e366e2ded30c5fe8d
# Parent  656e9412667cd40849db8d645a2e3c5168708a67
more uniform signature for various process invocations;
env refers to full environment, not the update;

diff -r 656e9412667c -r 4c89504c76fb src/Pure/System/bash.scala
--- 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
diff -r 656e9412667c -r 4c89504c76fb src/Pure/System/cygwin.scala
--- 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")
     }
   }
 }
diff -r 656e9412667c -r 4c89504c76fb src/Pure/System/isabelle_system.scala
--- 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)
     }
   }
diff -r 656e9412667c -r 4c89504c76fb src/Pure/Tools/build.scala
--- 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) =>
diff -r 656e9412667c -r 4c89504c76fb src/Pure/Tools/ml_process.scala
--- 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 =