equal
deleted
inserted
replaced
501 } |
501 } |
502 |
502 |
503 build_errors match { |
503 build_errors match { |
504 case Exn.Res(build_errs) => |
504 case Exn.Res(build_errs) => |
505 val errs = build_errs ::: document_errors |
505 val errs = build_errs ::: document_errors |
506 if (errs.isEmpty) result |
506 if (errs.nonEmpty) { |
507 else { |
|
508 result.error_rc.output( |
507 result.error_rc.output( |
509 errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: |
508 errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: |
510 errs.map(Protocol.Error_Message_Marker.apply)) |
509 errs.map(Protocol.Error_Message_Marker.apply)) |
511 } |
510 } |
|
511 else if (progress.stopped && result.ok) result.copy(rc = Process_Result.interrupt_rc) |
|
512 else result |
512 case Exn.Exn(Exn.Interrupt()) => |
513 case Exn.Exn(Exn.Interrupt()) => |
513 if (result.ok) result.copy(rc = Process_Result.interrupt_rc) else result |
514 if (result.ok) result.copy(rc = Process_Result.interrupt_rc) |
|
515 else result |
514 case Exn.Exn(exn) => throw exn |
516 case Exn.Exn(exn) => throw exn |
515 } |
517 } |
516 } |
518 } |
517 |
519 |
518 def terminate(): Unit = future_result.cancel() |
520 def terminate(): Unit = future_result.cancel() |