--- 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) }
--- 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 */