tuned signature;
authorwenzelm
Fri Sep 07 19:11:16 2018 +0200 (9 months ago)
changeset 6892701f46a4b22b4
parent 68926 5129fcc1b6c0
child 68928 835e5d45359c
tuned signature;
src/Pure/System/process_result.scala
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/System/process_result.scala	Fri Sep 07 17:08:47 2018 +0200
     1.2 +++ b/src/Pure/System/process_result.scala	Fri Sep 07 19:11:16 2018 +0200
     1.3 @@ -23,6 +23,8 @@
     1.4    def ok: Boolean = rc == 0
     1.5    def interrupted: Boolean = rc == Exn.Interrupt.return_code
     1.6  
     1.7 +  def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1)
     1.8 +
     1.9    def check_rc(pred: Int => Boolean): Process_Result =
    1.10      if (pred(rc)) this
    1.11      else if (interrupted) throw Exn.Interrupt()
     2.1 --- a/src/Pure/Tools/dump.scala	Fri Sep 07 17:08:47 2018 +0200
     2.2 +++ b/src/Pure/Tools/dump.scala	Fri Sep 07 19:11:16 2018 +0200
     2.3 @@ -163,8 +163,7 @@
     2.4  
     2.5      Consumer.shutdown().foreach(progress.echo_error_message(_))
     2.6  
     2.7 -    if (theories_result.ok) session_result
     2.8 -    else session_result.copy(rc = session_result.rc max 1)
     2.9 +    if (theories_result.ok) session_result else session_result.error_rc
    2.10    }
    2.11  
    2.12