# HG changeset patch
# User wenzelm
# Date 1455447812 -3600
# Node ID f868f12f94198fe736c4c950c858f1ecafc25bbb
# Parent  236e1ea5a197bf79e52394d96df424562e261021
tuned signature;

diff -r 236e1ea5a197 -r f868f12f9419 src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Sun Feb 14 11:52:27 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Sun Feb 14 12:03:32 2016 +0100
@@ -19,12 +19,13 @@
   {
     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 error(s: String, err_rc: Int = 0): Result =
+      copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
 
-    def check_error: Result =
+    def check: Result =
       if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-      else if (rc != 0) error(err)
+      else if (rc != 0) Library.error(err)
       else this
 
     def print: Result =
diff -r 236e1ea5a197 -r f868f12f9419 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Feb 14 11:52:27 2016 +0100
+++ b/src/Pure/Tools/build.scala	Sun Feb 14 12:03:32 2016 +0100
@@ -640,8 +640,8 @@
       timeout_request.foreach(_.cancel)
 
       if (res.rc == Exn.Interrupt.return_code) {
-        if (was_timeout) res.add_err(Output.error_text("Timeout")).set_rc(1)
-        else res.add_err(Output.error_text("Interrupt"))
+        if (was_timeout) res.error(Output.error_text("Timeout"), 1)
+        else res.error(Output.error_text("Interrupt"))
       }
       else res
     }
diff -r 236e1ea5a197 -r f868f12f9419 src/Pure/Tools/check_source.scala
--- a/src/Pure/Tools/check_source.scala	Sun Feb 14 11:52:27 2016 +0100
+++ b/src/Pure/Tools/check_source.scala	Sun Feb 14 12:03:32 2016 +0100
@@ -41,9 +41,9 @@
   def check_hg(root: Path)
   {
     Output.writeln("Checking " + root + " ...")
-    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check_error
+    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check
     for {
-      file <- Isabelle_System.hg("manifest", root).check_error.out_lines
+      file <- Isabelle_System.hg("manifest", root).check.out_lines
       if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
     } check_file(root + Path.explode(file))
   }