src/Pure/Concurrent/bash.scala

--- a/src/Pure/Concurrent/bash.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -26,20 +26,21 @@
     }
   }
 
-  def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
-    new Process(cwd, env, redirect, args:_*)
+  def process(script: String,
+      cwd: JFile = null, env: Map[String, String] = null, redirect: Boolean = false): Process =
+    new Process(script, cwd, env, redirect)
 
   class Process private [Bash](
-      cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
+      script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
     extends Prover.System_Process
   {
+    val script_file = Isabelle_System.tmp_file("bash_script")
+    File.write(script_file, script)
+
     private val proc =
-    {
-      val params =
-        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", "bash")
-      Isabelle_System.process(
-        cwd, Isabelle_System.settings(env), redirect, (params ::: args.toList):_*)
-    }
+      Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
+        File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
+          "bash", File.standard_path(script_file))
 
 
     // channels
@@ -90,14 +91,20 @@
     try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
     catch { case _: IllegalStateException => }
 
-    private def cleanup() =
+
+    /* join */
+
+    def join: Int =
+    {
+      val rc = proc.waitFor
+
       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
       catch { case _: IllegalStateException => }
 
+      script_file.delete
 
-    /* join */
-
-    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
+      rc
+    }
 
 
     /* result */