tuned signature;
authorwenzelm
Wed, 24 Feb 2016 22:03:24 +0100
changeset 62399 36e885190439
parent 62398 a4b68bf18f8d
child 62400 833af0d6d469
tuned signature;
src/Pure/Concurrent/bash.scala
src/Pure/Tools/build.scala
--- a/src/Pure/Concurrent/bash.scala	Wed Feb 24 16:00:57 2016 +0000
+++ b/src/Pure/Concurrent/bash.scala	Wed Feb 24 22:03:24 2016 +0100
@@ -23,10 +23,13 @@
     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 (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-      else if (rc != 0) Library.error(err)
-      else this
+      if (ok) this
+      else if (interrupted) throw Exn.Interrupt()
+      else Library.error(err)
 
     def print: Result =
     {
--- a/src/Pure/Tools/build.scala	Wed Feb 24 16:00:57 2016 +0000
+++ b/src/Pure/Tools/build.scala	Wed Feb 24 22:03:24 2016 +0100
@@ -632,7 +632,7 @@
     {
       val res = result.join
 
-      if (res.rc == 0 && !is_pure(name))
+      if (res.ok && !is_pure(name))
         Present.finish(progress, browser_info, graph_file, info, name)
 
       graph_file.delete
@@ -858,7 +858,7 @@
             progress.echo(res.err)
 
             val heap =
-              if (res.rc == 0) {
+              if (res.ok) {
                 (output_dir + log(name)).file.delete
 
                 val sources = make_stamp(name)