# HG changeset patch
# User wenzelm
# Date 1455450051 -3600
# Node ID e7a52a838a236ce0632e1d7955be4c44e54fdd27
# Parent  f868f12f94198fe736c4c950c858f1ecafc25bbb
more direct invocation of ISABELLE_BASH_PROCESS on Windows;

diff -r f868f12f9419 -r e7a52a838a23 src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Sun Feb 14 12:03:32 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Sun Feb 14 12:40:51 2016 +0100
@@ -47,10 +47,13 @@
       cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
     extends Prover.System_Process
   {
-    private val params =
-      List(Isabelle_System.getenv_strict("ISABELLE_BASH_PROCESS"), "-", "bash")
     private val proc =
-      Isabelle_System.execute_env(cwd, env, redirect, (params ::: args.toList):_*)
+    {
+      val params =
+        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", "bash")
+      Isabelle_System.process(
+        cwd, Isabelle_System.settings(env), redirect, (params ::: args.toList):_*)
+    }
 
 
     // channels
diff -r f868f12f9419 -r e7a52a838a23 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Feb 14 12:03:32 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Feb 14 12:40:51 2016 +0100
@@ -51,10 +51,10 @@
 
   @volatile private var _settings: Option[Map[String, String]] = None
 
-  def settings(): Map[String, String] =
+  def settings(env: Map[String, String] = null): Map[String, String] =
   {
     if (_settings.isEmpty) init()  // unsynchronized check
-    _settings.get
+    if (env == null) _settings.get else _settings.get ++ env
   }
 
   def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
@@ -133,7 +133,7 @@
 
   /* getenv */
 
-  def getenv(name: String): String = settings.getOrElse(name, "")
+  def getenv(name: String): String = settings().getOrElse(name, "")
 
   def getenv_strict(name: String): String =
   {
@@ -216,8 +216,7 @@
     val cmdline =
       if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ::: args.toList
       else args
-    val env1 = if (env == null) settings else settings ++ env
-    process(cwd, env1, redirect, cmdline: _*)
+    process(cwd, settings(env), redirect, cmdline: _*)
   }
 
   def execute(redirect: Boolean, args: String*): Process =