src/Pure/System/process_result.scala
changeset 62400 833af0d6d469
child 62401 15a2533f1f0a
equal deleted inserted replaced
62399:36e885190439 62400:833af0d6d469
       
     1 /*  Title:      Pure/System/process_result.scala
       
     2     Author:     Makarius
       
     3 
       
     4 Result of system process.
       
     5 */
       
     6 
       
     7 package isabelle
       
     8 
       
     9 final case class Process_Result(out_lines: List[String], err_lines: List[String], rc: Int)
       
    10 {
       
    11   def out: String = cat_lines(out_lines)
       
    12   def err: String = cat_lines(err_lines)
       
    13 
       
    14   def error(s: String, err_rc: Int = 0): Process_Result =
       
    15     copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
       
    16 
       
    17   def ok: Boolean = rc == 0
       
    18   def interrupted: Boolean = rc == Exn.Interrupt.return_code
       
    19 
       
    20   def check: Process_Result =
       
    21     if (ok) this
       
    22     else if (interrupted) throw Exn.Interrupt()
       
    23     else Library.error(err)
       
    24 
       
    25   def print: Process_Result =
       
    26   {
       
    27     Output.warning(Library.trim_line(err))
       
    28     Output.writeln(Library.trim_line(out))
       
    29     Process_Result(Nil, Nil, rc)
       
    30   }
       
    31 }