src/Pure/System/bash.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/bash.scala	Thu Mar 10 09:50:53 2016 +0100
@@ -0,0 +1,168 @@
+/*  Title:      Pure/System/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)
+    }
+  }
+}