clarified modules;

--- a/src/Pure/Concurrent/bash.scala	Wed Feb 24 22:03:24 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Wed Feb 24 22:11:28 2016 +0100
@@ -13,36 +13,6 @@
 
 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 error(s: String, err_rc: Int = 0): Result =
-      copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
-
-    def ok: Boolean = rc == 0
-    def interrupted: Boolean = rc == Exn.Interrupt.return_code
-
-    def check: Result =
-      if (ok) this
-      else if (interrupted) throw Exn.Interrupt()
-      else Library.error(err)
-
-    def print: Result =
-    {
-      Output.warning(Library.trim_line(err))
-      Output.writeln(Library.trim_line(out))
-      Result(Nil, Nil, rc)
-    }
-  }
-
-
-
-  /** process **/
-
   def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
     new Process(cwd, env, redirect, args:_*)
 

--- a/src/Pure/System/isabelle_system.scala	Wed Feb 24 22:03:24 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Wed Feb 24 22:11:28 2016 +0100
@@ -319,7 +319,7 @@
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
     progress_limit: Option[Long] = None,
-    strict: Boolean = true): Bash.Result =
+    strict: Boolean = true): Process_Result =
   {
     with_tmp_file("isabelle_script") { script_file =>
       File.write(script_file, script)
@@ -337,7 +337,7 @@
         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)
+      Process_Result(stdout.join, stderr.join, rc)
     }
   }
 
@@ -367,10 +367,11 @@
   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): Process_Result =
     bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
 
 
+
   /** Isabelle resources **/
 
   /* components */

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/process_result.scala	Wed Feb 24 22:11:28 2016 +0100
@@ -0,0 +1,31 @@
+/*  Title:      Pure/System/process_result.scala
+    Author:     Makarius
+
+Result of system process.
+*/
+
+package isabelle
+
+final case class Process_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 error(s: String, err_rc: Int = 0): Process_Result =
+    copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
+
+  def ok: Boolean = rc == 0
+  def interrupted: Boolean = rc == Exn.Interrupt.return_code
+
+  def check: Process_Result =
+    if (ok) this
+    else if (interrupted) throw Exn.Interrupt()
+    else Library.error(err)
+
+  def print: Process_Result =
+  {
+    Output.warning(Library.trim_line(err))
+    Output.writeln(Library.trim_line(out))
+    Process_Result(Nil, Nil, rc)
+  }
+}

--- a/src/Pure/Tools/build.scala	Wed Feb 24 22:03:24 2016 +0100
+++ b/src/Pure/Tools/build.scala	Wed Feb 24 22:11:28 2016 +0100
@@ -628,7 +628,7 @@
       else None
     }
 
-    def join: Bash.Result =
+    def join: Process_Result =
     {
       val res = result.join
 

--- a/src/Pure/build-jars	Wed Feb 24 22:03:24 2016 +0100
+++ b/src/Pure/build-jars	Wed Feb 24 22:11:28 2016 +0100
@@ -82,6 +82,7 @@
   System/options.scala
   System/platform.scala
   System/posix_interrupt.scala
+  System/process_result.scala
   System/progress.scala
   System/system_channel.scala
   System/utf8.scala