clarified signature;

--- a/src/Pure/System/bash.scala	Mon Jun 28 20:02:32 2021 +0200
+++ b/src/Pure/System/bash.scala	Mon Jun 28 20:52:31 2021 +0200
@@ -59,8 +59,7 @@
     }
     cmd.add("-c")
     cmd.add("kill -" + signal + " -" + group_pid)
-    val (_, rc) = Isabelle_Env.process_output(Isabelle_Env.process(cmd))
-    rc == 0
+    Isabelle_Env.exec_process(cmd).ok
   }
 
   def process(script: String,
@@ -95,10 +94,10 @@
     File.write(script_file, winpid_script)
 
     private val proc =
-      Isabelle_Env.process(
+      Isabelle_Env.process_builder(
         JList.of(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)
+        cwd = cwd, env = env, redirect = redirect).start()
 
 
     // channels

--- a/src/Pure/System/isabelle_env.scala	Mon Jun 28 20:02:32 2021 +0200
+++ b/src/Pure/System/isabelle_env.scala	Mon Jun 28 20:52:31 2021 +0200
@@ -61,13 +61,12 @@
   {
     require(Platform.is_windows, "Windows platform expected")
 
-    def exec(cmdline: JList[String]): Unit =
+    def cygwin_exec(cmd: JList[String]): Unit =
     {
       val cwd = new JFile(isabelle_root)
       val env = sys.env + ("CYGWIN" -> "nodosfilewarning")
-      val (output, rc) =
-        Isabelle_Env.process_output(Isabelle_Env.process(cmdline, cwd = cwd, env = env, redirect = true))
-      if (rc != 0) error(output)
+      val res = exec_process(cmd, cwd = cwd, env = env, redirect = true)
+      if (!res.ok) error(res.out)
     }
 
     val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
@@ -91,8 +90,8 @@
       }
       recover_symlinks(symlinks)
 
-      exec(JList.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall"))
-      exec(JList.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall"))
+      cygwin_exec(JList.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall"))
+      cygwin_exec(JList.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall"))
     }
   }
 
@@ -102,40 +101,63 @@
 
   /* raw process */
 
-  def process(command_line: JList[String],
+  def process_builder(cmd: JList[String],
     cwd: JFile = null,
     env: Map[String, String] = settings(),
-    redirect: Boolean = false): Process =
+    redirect: Boolean = false): ProcessBuilder =
   {
-    val proc = new ProcessBuilder
+    val builder = new ProcessBuilder
 
     // fragile on Windows:
     // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
-    proc.command(command_line)
+    builder.command(cmd)
 
-    if (cwd != null) proc.directory(cwd)
+    if (cwd != null) builder.directory(cwd)
     if (env != null) {
-      proc.environment.clear()
-      for ((x, y) <- env) proc.environment.put(x, y)
+      builder.environment.clear()
+      for ((x, y) <- env) builder.environment.put(x, y)
     }
-    proc.redirectErrorStream(redirect)
-    proc.start
+    builder.redirectErrorStream(redirect)
+  }
+
+  class Exec_Result(val rc: Int, val out: String, val err: String)
+  {
+    def ok: Boolean = rc == 0
   }
 
-  def process_output(proc: Process): (String, Int) =
+  def exec_process(command_line: JList[String],
+    cwd: JFile = null,
+    env: Map[String, String] = settings(),
+    redirect: Boolean = false): Exec_Result =
   {
-    proc.getOutputStream.close()
-
-    val output = File.read_stream(proc.getInputStream)
-    val rc =
-      try { proc.waitFor }
+    val out_file = Files.createTempFile(null, null)
+    val err_file = Files.createTempFile(null, null)
+    try {
+      val proc =
+      {
+        val builder = process_builder(command_line, cwd = cwd, env = env, redirect = redirect)
+        builder.redirectOutput(out_file.toFile)
+        builder.redirectError(err_file.toFile)
+        builder.start()
+      }
+      proc.getOutputStream.close()
+      try { proc.waitFor() }
       finally {
         proc.getInputStream.close()
         proc.getErrorStream.close()
         proc.destroy()
-        Exn.Interrupt.dispose()
+        Thread.interrupted()
       }
-    (output, rc)
+
+      val rc = proc.exitValue()
+      val out = Files.readString(out_file)
+      val err = Files.readString(err_file)
+      new Exec_Result(rc, out, err)
+    }
+    finally {
+      Files.deleteIfExists(out_file)
+      Files.deleteIfExists(err_file)
+    }
   }
 
 
@@ -210,8 +232,8 @@
           cmd.add("-d")
           cmd.add(dump.toString)
 
-          val (output, rc) = process_output(process(cmd, env = env, redirect = true))
-          if (rc != 0) error(output)
+          val res = exec_process(cmd, env = env, redirect = true)
+          if (!res.ok) error(res.out)
 
           val entries =
             space_explode('\u0000', File.read(dump)).flatMap(