author | wenzelm |
Fri, 23 Jun 2017 14:38:32 +0200 | |
changeset 66176 | b51a40281016 |
parent 64408 | 50bcf976f276 |
child 68091 | 0c7820590236 |
permissions | -rw-r--r-- |
62400 | 1 |
/* Title: Pure/System/process_result.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Result of system process. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
62401 | 9 |
final case class Process_Result( |
62402 | 10 |
rc: Int, |
11 |
out_lines: List[String] = Nil, |
|
12 |
err_lines: List[String] = Nil, |
|
62569 | 13 |
timeout: Boolean = false, |
14 |
timing: Timing = Timing.zero) |
|
62400 | 15 |
{ |
16 |
def out: String = cat_lines(out_lines) |
|
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 | 19 |
|
62569 | 20 |
def was_timeout: Process_Result = copy(rc = 1, timeout = true) |
62401 | 21 |
|
62400 | 22 |
def ok: Boolean = rc == 0 |
23 |
def interrupted: Boolean = rc == Exn.Interrupt.return_code |
|
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 | 27 |
else if (interrupted) throw Exn.Interrupt() |
62492 | 28 |
else Exn.error(err) |
62400 | 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 | 32 |
def print: Process_Result = |
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 | 37 |
} |
62553 | 38 |
|
39 |
def print_stdout: Process_Result = |
|
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 | 43 |
copy(out_lines = Nil, err_lines = Nil) |
44 |
} |
|
64024 | 45 |
|
46 |
def print_if(b: Boolean): Process_Result = if (b) print else this |
|
47 |
def print_stdout_if(b: Boolean): Process_Result = if (b) print_stdout else this |
|
62400 | 48 |
} |