src/Pure/System/process_result.scala
changeset 75393 87ebf5a50283
parent 74306 a117c076aa22
child 77243 629dce95bb5c
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
     4 Result of system process.
     4 Result of system process.
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 object Process_Result
     9 object Process_Result {
    10 {
       
    11   /* return code */
    10   /* return code */
    12 
    11 
    13   object RC
    12   object RC {
    14   {
       
    15     val ok = 0
    13     val ok = 0
    16     val error = 1
    14     val error = 1
    17     val failure = 2
    15     val failure = 2
    18     val interrupt = 130
    16     val interrupt = 130
    19     val timeout = 142
    17     val timeout = 142
    20 
    18 
    21     private def text(rc: Int): String =
    19     private def text(rc: Int): String = {
    22     {
       
    23       val txt =
    20       val txt =
    24         rc match {
    21         rc match {
    25           case `ok` => "OK"
    22           case `ok` => "OK"
    26           case `error` => "ERROR"
    23           case `error` => "ERROR"
    27           case `failure` => "FAILURE"
    24           case `failure` => "FAILURE"
    45 
    42 
    46 final case class Process_Result(
    43 final case class Process_Result(
    47   rc: Int,
    44   rc: Int,
    48   out_lines: List[String] = Nil,
    45   out_lines: List[String] = Nil,
    49   err_lines: List[String] = Nil,
    46   err_lines: List[String] = Nil,
    50   timing: Timing = Timing.zero)
    47   timing: Timing = Timing.zero
    51 {
    48 ) {
    52   def out: String = Library.trim_line(cat_lines(out_lines))
    49   def out: String = Library.trim_line(cat_lines(out_lines))
    53   def err: String = Library.trim_line(cat_lines(err_lines))
    50   def err: String = Library.trim_line(cat_lines(err_lines))
    54 
    51 
    55   def output(outs: List[String]): Process_Result =
    52   def output(outs: List[String]): Process_Result =
    56     copy(out_lines = out_lines ::: outs.flatMap(split_lines))
    53     copy(out_lines = out_lines ::: outs.flatMap(split_lines))
    79   def check: Process_Result = check_rc(_ == Process_Result.RC.ok)
    76   def check: Process_Result = check_rc(_ == Process_Result.RC.ok)
    80 
    77 
    81   def print_return_code: String = Process_Result.RC.print_long(rc)
    78   def print_return_code: String = Process_Result.RC.print_long(rc)
    82   def print_rc: String = Process_Result.RC.print(rc)
    79   def print_rc: String = Process_Result.RC.print(rc)
    83 
    80 
    84   def print: Process_Result =
    81   def print: Process_Result = {
    85   {
       
    86     Output.warning(err)
    82     Output.warning(err)
    87     Output.writeln(out)
    83     Output.writeln(out)
    88     copy(out_lines = Nil, err_lines = Nil)
    84     copy(out_lines = Nil, err_lines = Nil)
    89   }
    85   }
    90 
    86 
    91   def print_stdout: Process_Result =
    87   def print_stdout: Process_Result = {
    92   {
       
    93     Output.warning(err, stdout = true)
    88     Output.warning(err, stdout = true)
    94     Output.writeln(out, stdout = true)
    89     Output.writeln(out, stdout = true)
    95     copy(out_lines = Nil, err_lines = Nil)
    90     copy(out_lines = Nil, err_lines = Nil)
    96   }
    91   }
    97 }
    92 }