# HG changeset patch
# User wenzelm
# Date 1457358808 -3600
# Node ID 57f379ef662fbeee5e86cd3d6036c04fcb5941e8
# Parent  b27b7c2200b902a6291cf64b8607daf617ec15ef
clarified modules;

diff -r b27b7c2200b9 -r 57f379ef662f src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Mon Mar 07 09:49:58 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Mon Mar 07 14:53:28 2016 +0100
@@ -13,6 +13,19 @@
 
 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(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
     new Process(cwd, env, redirect, args:_*)
 
@@ -82,8 +95,33 @@
       catch { case _: IllegalStateException => }
 
 
-    /* result */
+    /* 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)
+    }
   }
 }
diff -r b27b7c2200b9 -r 57f379ef662f src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 07 09:49:58 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Mar 07 14:53:28 2016 +0100
@@ -302,19 +302,6 @@
 
   /* bash */
 
-  private class Limited_Progress(proc: Bash.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 bash(script: String, cwd: JFile = null, env: Map[String, String] = null,
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
@@ -323,21 +310,8 @@
   {
     with_tmp_file("isabelle_script") { script_file =>
       File.write(script_file, script)
-      val proc = Bash.process(cwd, env, false, File.standard_path(script_file))
-      proc.stdin.close
-
-      val limited = new Limited_Progress(proc, progress_limit)
-      val stdout =
-        Future.thread("bash_stdout") { File.read_lines(proc.stdout, limited(progress_stdout)) }
-      val stderr =
-        Future.thread("bash_stderr") { File.read_lines(proc.stderr, limited(progress_stderr)) }
-
-      val rc =
-        try { proc.join }
-        catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
-      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-
-      Process_Result(rc, out_lines = stdout.join, err_lines = stderr.join)
+      Bash.process(cwd, env, false, File.standard_path(script_file)).
+        result(progress_stdout, progress_stderr, progress_limit, strict)
     }
   }