src/Pure/System/process_result.scala
author wenzelm
Fri, 23 Jun 2017 14:38:32 +0200
changeset 66176 b51a40281016
parent 64408 50bcf976f276
child 68091 0c7820590236
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62400
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/process_result.scala
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
     3
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
     4
Result of system process.
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
     6
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
     8
62401
15a2533f1f0a more informative Process_Result;
wenzelm
parents: 62400
diff changeset
     9
final case class Process_Result(
62402
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
    10
  rc: Int,
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
    11
  out_lines: List[String] = Nil,
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
    12
  err_lines: List[String] = Nil,
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62553
diff changeset
    13
  timeout: Boolean = false,
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62553
diff changeset
    14
  timing: Timing = Timing.zero)
62400
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    15
{
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    16
  def out: String = cat_lines(out_lines)
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    17
  def err: String = cat_lines(err_lines)
62405
d653532762e4 proper return code for timeout (amending f868f12f9419);
wenzelm
parents: 62404
diff changeset
    18
  def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
62400
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    19
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62553
diff changeset
    20
  def was_timeout: Process_Result = copy(rc = 1, timeout = true)
62401
15a2533f1f0a more informative Process_Result;
wenzelm
parents: 62400
diff changeset
    21
62400
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    22
  def ok: Boolean = rc == 0
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    23
  def interrupted: Boolean = rc == Exn.Interrupt.return_code
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    24
64408
50bcf976f276 clarified hg push return code: 1 means "nothing to push";
wenzelm
parents: 64138
diff changeset
    25
  def check_rc(pred: Int => Boolean): Process_Result =
50bcf976f276 clarified hg push return code: 1 means "nothing to push";
wenzelm
parents: 64138
diff changeset
    26
    if (pred(rc)) this
62400
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    27
    else if (interrupted) throw Exn.Interrupt()
62492
0e53fade87fe clarified modules;
wenzelm
parents: 62405
diff changeset
    28
    else Exn.error(err)
62400
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    29
64408
50bcf976f276 clarified hg push return code: 1 means "nothing to push";
wenzelm
parents: 64138
diff changeset
    30
  def check: Process_Result = check_rc(_ == 0)
50bcf976f276 clarified hg push return code: 1 means "nothing to push";
wenzelm
parents: 64138
diff changeset
    31
62400
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    32
  def print: Process_Result =
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    33
  {
64138
cf0c8c5782af eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
wenzelm
parents: 64024
diff changeset
    34
    Output.warning(err)
cf0c8c5782af eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
wenzelm
parents: 64024
diff changeset
    35
    Output.writeln(out)
62404
13a0f537e232 retain tail out_lines as printed, but not the whole log content;
wenzelm
parents: 62402
diff changeset
    36
    copy(out_lines = Nil, err_lines = Nil)
62400
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    37
  }
62553
d2e0d626fb96 tuned signature;
wenzelm
parents: 62492
diff changeset
    38
d2e0d626fb96 tuned signature;
wenzelm
parents: 62492
diff changeset
    39
  def print_stdout: Process_Result =
d2e0d626fb96 tuned signature;
wenzelm
parents: 62492
diff changeset
    40
  {
64138
cf0c8c5782af eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
wenzelm
parents: 64024
diff changeset
    41
    Output.warning(err, stdout = true)
cf0c8c5782af eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
wenzelm
parents: 64024
diff changeset
    42
    Output.writeln(out, stdout = true)
62553
d2e0d626fb96 tuned signature;
wenzelm
parents: 62492
diff changeset
    43
    copy(out_lines = Nil, err_lines = Nil)
d2e0d626fb96 tuned signature;
wenzelm
parents: 62492
diff changeset
    44
  }
64024
3dd92c391eca more operations;
wenzelm
parents: 62569
diff changeset
    45
3dd92c391eca more operations;
wenzelm
parents: 62569
diff changeset
    46
  def print_if(b: Boolean): Process_Result = if (b) print else this
3dd92c391eca more operations;
wenzelm
parents: 62569
diff changeset
    47
  def print_stdout_if(b: Boolean): Process_Result = if (b) print_stdout else this
62400
833af0d6d469 clarified modules;
wenzelm
parents:
diff changeset
    48
}