# HG changeset patch
# User wenzelm
# Date 1440095766 -7200
# Node ID 2fc5a44346b5ab2531c04cbe0e15f4a06698c7af
# Parent  07592e2171801e67eaab53f37fb68cb99ae0e46f
clarified modules, like ML version;

diff -r 07592e217180 -r 2fc5a44346b5 src/Pure/Concurrent/bash.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash.scala	Thu Aug 20 20:36:06 2015 +0200
@@ -0,0 +1,106 @@
+/*  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
+{
+  /** result **/
+
+  final case class Result(out_lines: List[String], err_lines: List[String], rc: Int)
+  {
+    def out: String = cat_lines(out_lines)
+    def err: String = cat_lines(err_lines)
+    def add_err(s: String): Result = copy(err_lines = err_lines ::: List(s))
+    def set_rc(i: Int): Result = copy(rc = i)
+
+    def check_error: Result =
+      if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+      else if (rc != 0) error(err)
+      else this
+  }
+
+
+
+  /** process **/
+
+  def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
+    new Process(cwd, env, redirect, args:_*)
+
+  class Process private [Bash](
+      cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
+    extends Prover.System_Process
+  {
+    private val params =
+      List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
+    private val proc = Isabelle_System.execute_env(cwd, env, redirect, (params ::: args.toList):_*)
+
+
+    // 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
+
+    private def kill_cmd(signal: String): Int =
+      Isabelle_System.execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid)
+        .waitFor
+
+    private def kill(signal: String): Boolean =
+      Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 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 interrupt() { multi_kill("INT") }
+    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
+
+
+    // JVM shutdown hook
+
+    private val shutdown_hook = new Thread { override def run = terminate() }
+
+    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
+    catch { case _: IllegalStateException => }
+
+    private def cleanup() =
+      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
+      catch { case _: IllegalStateException => }
+
+
+    /* result */
+
+    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
+  }
+}
diff -r 07592e217180 -r 2fc5a44346b5 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Aug 20 19:33:26 2015 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Aug 20 20:36:06 2015 +0200
@@ -19,9 +19,7 @@
         val cmdline =
           Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
             (system_channel.prover_args ::: prover_args)
-        val process =
-          new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
-            Prover.System_Process
+        val process = Bash.process(null, null, false, cmdline: _*)
         process.stdin.close
         process
       }
diff -r 07592e217180 -r 2fc5a44346b5 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Aug 20 19:33:26 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Aug 20 20:36:06 2015 +0200
@@ -9,8 +9,7 @@
 
 
 import java.util.regex.Pattern
-import java.io.{File => JFile, BufferedReader, InputStreamReader,
-  BufferedWriter, OutputStreamWriter, IOException}
+import java.io.{File => JFile, IOException}
 import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
 import java.nio.file.attribute.BasicFileAttributes
 import java.net.{URL, URLDecoder, MalformedURLException}
@@ -294,75 +293,6 @@
     execute_env(null, null, redirect, args: _*)
 
 
-  /* managed process */
-
-  class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
-  {
-    private val params =
-      List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
-    private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*)
-
-
-    // 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
-
-    private def kill_cmd(signal: String): Int =
-      execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid).waitFor
-
-    private def kill(signal: String): Boolean =
-      Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 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 interrupt() { multi_kill("INT") }
-    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
-
-
-    // JVM shutdown hook
-
-    private val shutdown_hook = new Thread { override def run = terminate() }
-
-    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
-    catch { case _: IllegalStateException => }
-
-    private def cleanup() =
-      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
-      catch { case _: IllegalStateException => }
-
-
-    /* result */
-
-    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
-  }
-
-
   /* tmp files */
 
   private def isabelle_tmp_prefix(): JFile =
@@ -430,20 +360,7 @@
 
   /* bash */
 
-  final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
-  {
-    def out: String = cat_lines(out_lines)
-    def err: String = cat_lines(err_lines)
-    def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
-    def set_rc(i: Int): Bash_Result = copy(rc = i)
-
-    def check_error: Bash_Result =
-      if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-      else if (rc != 0) error(err)
-      else this
-  }
-
-  private class Limited_Progress(proc: Managed_Process, progress_limit: Option[Long])
+  private class Limited_Progress(proc: Bash.Process, progress_limit: Option[Long])
   {
     private var count = 0L
     def apply(progress: String => Unit)(line: String): Unit = synchronized {
@@ -460,11 +377,11 @@
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
     progress_limit: Option[Long] = None,
-    strict: Boolean = true): Bash_Result =
+    strict: Boolean = true): Bash.Result =
   {
     with_tmp_file("isabelle_script") { script_file =>
       File.write(script_file, script)
-      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
+      val proc = Bash.process(cwd, env, false, "bash", posix_path(script_file))
       proc.stdin.close
 
       val limited = new Limited_Progress(proc, progress_limit)
@@ -482,11 +399,11 @@
         catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
-      Bash_Result(stdout.join, stderr.join, rc)
+      Bash.Result(stdout.join, stderr.join, rc)
     }
   }
 
-  def bash(script: String): Bash_Result = bash_env(null, null, script)
+  def bash(script: String): Bash.Result = bash_env(null, null, script)
 
 
   /* system tools */
@@ -514,7 +431,7 @@
   def pdf_viewer(arg: Path): Unit =
     bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
 
-  def hg(cmd_line: String, cwd: Path = Path.current): Bash_Result =
+  def hg(cmd_line: String, cwd: Path = Path.current): Bash.Result =
     bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
 
 
diff -r 07592e217180 -r 2fc5a44346b5 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Aug 20 19:33:26 2015 +0200
+++ b/src/Pure/Tools/build.scala	Thu Aug 20 20:36:06 2015 +0200
@@ -653,7 +653,7 @@
       else None
     }
 
-    def join: Isabelle_System.Bash_Result =
+    def join: Bash.Result =
     {
       val res = result.join
 
diff -r 07592e217180 -r 2fc5a44346b5 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Aug 20 19:33:26 2015 +0200
+++ b/src/Pure/build-jars	Thu Aug 20 20:36:06 2015 +0200
@@ -9,6 +9,7 @@
 ## sources
 
 declare -a SOURCES=(
+  Concurrent/bash.scala
   Concurrent/consumer_thread.scala
   Concurrent/counter.scala
   Concurrent/event_timer.scala