src/Pure/System/process_result.scala
changeset 62569 5db10482f4cf
parent 62553 d2e0d626fb96
child 64024 3dd92c391eca
equal deleted inserted replaced
62568:3541bc1e97d2 62569:5db10482f4cf
     8 
     8 
     9 final case class Process_Result(
     9 final case class Process_Result(
    10   rc: Int,
    10   rc: Int,
    11   out_lines: List[String] = Nil,
    11   out_lines: List[String] = Nil,
    12   err_lines: List[String] = Nil,
    12   err_lines: List[String] = Nil,
    13   timeout: Option[Time] = None)
    13   timeout: Boolean = false,
       
    14   timing: Timing = Timing.zero)
    14 {
    15 {
    15   def out: String = cat_lines(out_lines)
    16   def out: String = cat_lines(out_lines)
    16   def err: String = cat_lines(err_lines)
    17   def err: String = cat_lines(err_lines)
    17   def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
    18   def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
    18 
    19 
    19   def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t))
    20   def was_timeout: Process_Result = copy(rc = 1, timeout = true)
    20 
    21 
    21   def ok: Boolean = rc == 0
    22   def ok: Boolean = rc == 0
    22   def interrupted: Boolean = rc == Exn.Interrupt.return_code
    23   def interrupted: Boolean = rc == Exn.Interrupt.return_code
    23 
    24 
    24   def check: Process_Result =
    25   def check: Process_Result =