# HG changeset patch
# User wenzelm
# Date 1342720964 -7200
# Node ID bcce872202b3ec9acaeed94f67765739de61efd6
# Parent  7fbf98ee265fad54fa7688b2f9d526a1f326c943
support external processes with explicit environment;

diff -r 7fbf98ee265f -r bcce872202b3 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Jul 19 19:12:58 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Jul 19 20:02:44 2012 +0200
@@ -137,7 +137,7 @@
       val cmdline =
         Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
           (system_channel.isabelle_args ::: args)
-      new Isabelle_System.Managed_Process(false, cmdline: _*)
+      new Isabelle_System.Managed_Process(null, null, false, cmdline: _*)
     }
     catch { case e: IOException => system_channel.accepted(); throw(e) }
 
diff -r 7fbf98ee265f -r bcce872202b3 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Jul 19 19:12:58 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Jul 19 20:02:44 2012 +0200
@@ -160,22 +160,26 @@
 
   /* plain execute */
 
-  def execute(redirect: Boolean, args: String*): Process =
+  def execute_env(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
   {
     val cmdline =
       if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
       else args
-    Standard_System.raw_execute(null, settings, redirect, cmdline: _*)
+    val env1 = if (env == null) settings else settings ++ env
+    Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*)
   }
 
+  def execute(redirect: Boolean, args: String*): Process =
+    execute_env(null, null, redirect, args: _*)
+
 
   /* managed process */
 
-  class Managed_Process(redirect: Boolean, args: String*)
+  class Managed_Process(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
   {
     private val params =
       List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
-    private val proc = execute(redirect, (params ++ args):_*)
+    private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
 
 
     // channels
@@ -238,11 +242,11 @@
 
   /* bash */
 
-  def bash(script: String): (String, String, Int) =
+  def bash_env(cwd: File, env: Map[String, String], script: String): (String, String, Int) =
   {
     Standard_System.with_tmp_file("isabelle_script") { script_file =>
       Standard_System.write_file(script_file, script)
-      val proc = new Managed_Process(false, "bash", posix_path(script_file.getPath))
+      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
 
       proc.stdin.close
       val stdout = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
@@ -255,6 +259,8 @@
     }
   }
 
+  def bash(script: String): (String, String, Int) = bash_env(null, null, script)
+
 
   /* system tools */