tuned signature;
authorwenzelm
Sun Feb 14 12:03:32 2016 +0100 (2016-02-14)
changeset 62303f868f12f9419
parent 62302 236e1ea5a197
child 62304 e7a52a838a23
tuned signature;
src/Pure/Concurrent/bash.scala
src/Pure/Tools/build.scala
src/Pure/Tools/check_source.scala
     1.1 --- a/src/Pure/Concurrent/bash.scala	Sun Feb 14 11:52:27 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/bash.scala	Sun Feb 14 12:03:32 2016 +0100
     1.3 @@ -19,12 +19,13 @@
     1.4    {
     1.5      def out: String = cat_lines(out_lines)
     1.6      def err: String = cat_lines(err_lines)
     1.7 -    def add_err(s: String): Result = copy(err_lines = err_lines ::: List(s))
     1.8 -    def set_rc(i: Int): Result = copy(rc = i)
     1.9  
    1.10 -    def check_error: Result =
    1.11 +    def error(s: String, err_rc: Int = 0): Result =
    1.12 +      copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
    1.13 +
    1.14 +    def check: Result =
    1.15        if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
    1.16 -      else if (rc != 0) error(err)
    1.17 +      else if (rc != 0) Library.error(err)
    1.18        else this
    1.19  
    1.20      def print: Result =
     2.1 --- a/src/Pure/Tools/build.scala	Sun Feb 14 11:52:27 2016 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Sun Feb 14 12:03:32 2016 +0100
     2.3 @@ -640,8 +640,8 @@
     2.4        timeout_request.foreach(_.cancel)
     2.5  
     2.6        if (res.rc == Exn.Interrupt.return_code) {
     2.7 -        if (was_timeout) res.add_err(Output.error_text("Timeout")).set_rc(1)
     2.8 -        else res.add_err(Output.error_text("Interrupt"))
     2.9 +        if (was_timeout) res.error(Output.error_text("Timeout"), 1)
    2.10 +        else res.error(Output.error_text("Interrupt"))
    2.11        }
    2.12        else res
    2.13      }
     3.1 --- a/src/Pure/Tools/check_source.scala	Sun Feb 14 11:52:27 2016 +0100
     3.2 +++ b/src/Pure/Tools/check_source.scala	Sun Feb 14 12:03:32 2016 +0100
     3.3 @@ -41,9 +41,9 @@
     3.4    def check_hg(root: Path)
     3.5    {
     3.6      Output.writeln("Checking " + root + " ...")
     3.7 -    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check_error
     3.8 +    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check
     3.9      for {
    3.10 -      file <- Isabelle_System.hg("manifest", root).check_error.out_lines
    3.11 +      file <- Isabelle_System.hg("manifest", root).check.out_lines
    3.12        if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
    3.13      } check_file(root + Path.explode(file))
    3.14    }