diff -r 8c7301325f9f -r adffc55a682d src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Thu Mar 10 19:15:06 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,168 +0,0 @@
-/*  Title:      Pure/Concurrent/bash.scala
-    Author:     Makarius
-
-GNU bash processes, with propagation of interrupts.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile, BufferedReader, InputStreamReader,
-  BufferedWriter, OutputStreamWriter}
-
-
-object Bash
-{
-  private class Limited_Progress(proc: Process, progress_limit: Option[Long])
-  {
-    private var count = 0L
-    def apply(progress: String => Unit)(line: String): Unit = synchronized {
-      progress(line)
-      count = count + line.length + 1
-      progress_limit match {
-        case Some(limit) if count > limit => proc.terminate
-        case _ =>
-      }
-    }
-  }
-
-  def process(script: String,
-      cwd: JFile = null,
-      env: Map[String, String] = Map.empty,
-      redirect: Boolean = false): Process =
-    new Process(script, cwd, env, redirect)
-
-  class Process private [Bash](
-      script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
-    extends Prover.System_Process
-  {
-    private val timing_file = Isabelle_System.tmp_file("bash_script")
-    private val timing = Synchronized[Option[Timing]](None)
-
-    private val script_file = Isabelle_System.tmp_file("bash_script")
-    File.write(script_file, script)
-
-    private val proc =
-      Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
-        File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
-          File.standard_path(timing_file), "bash", File.standard_path(script_file))
-
-
-    // channels
-
-    val stdin: BufferedWriter =
-      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
-
-    val stdout: BufferedReader =
-      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
-
-    val stderr: BufferedReader =
-      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
-
-
-    // signals
-
-    private val pid = stdout.readLine
-
-    def interrupt()
-    { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
-
-    private def kill(signal: String): Boolean =
-      Exn.Interrupt.postpone {
-        Isabelle_System.kill(signal, pid)
-        Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
-
-    private def multi_kill(signal: String): Boolean =
-    {
-      var running = true
-      var count = 10
-      while (running && count > 0) {
-        if (kill(signal)) {
-          Exn.Interrupt.postpone {
-            Thread.sleep(100)
-            count -= 1
-          }
-        }
-        else running = false
-      }
-      running
-    }
-
-    def terminate()
-    {
-      multi_kill("INT") && multi_kill("TERM") && kill("KILL")
-      proc.destroy
-      cleanup()
-    }
-
-
-    // JVM shutdown hook
-
-    private val shutdown_hook = new Thread { override def run = terminate() }
-
-    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
-    catch { case _: IllegalStateException => }
-
-
-    // cleanup
-
-    private def cleanup()
-    {
-      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
-      catch { case _: IllegalStateException => }
-
-      script_file.delete
-
-      timing.change {
-        case None =>
-          if (timing_file.isFile) {
-            val t =
-              Word.explode(File.read(timing_file)) match {
-                case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
-                  Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
-                case _ => Timing.zero
-              }
-            timing_file.delete
-            Some(t)
-          }
-          else Some(Timing.zero)
-        case some => some
-      }
-    }
-
-
-    // join
-
-    def join: Int =
-    {
-      val rc = proc.waitFor
-      cleanup()
-      rc
-    }
-
-
-    // result
-
-    def result(
-      progress_stdout: String => Unit = (_: String) => (),
-      progress_stderr: String => Unit = (_: String) => (),
-      progress_limit: Option[Long] = None,
-      strict: Boolean = true): Process_Result =
-    {
-      stdin.close
-
-      val limited = new Limited_Progress(this, progress_limit)
-      val out_lines =
-        Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
-      val err_lines =
-        Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
-
-      val rc =
-        try { join }
-        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
-      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-
-      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
-    }
-  }
-}