author | wenzelm |
Mon, 26 Jul 2021 13:04:55 +0200 | |
changeset 74067 | 0b1462ce5fda |
parent 73277 | 0110e2e2964c |
child 74306 | a117c076aa22 |
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 |
||
71747 | 9 |
object Process_Result |
10 |
{ |
|
71749 | 11 |
def print_return_code(rc: Int): String = "Return code: " + rc + rc_text(rc) |
12 |
def print_rc(rc: Int): String = "return code " + rc + rc_text(rc) |
|
13 |
||
14 |
def rc_text(rc: Int): String = |
|
15 |
return_code_text.get(rc) match { |
|
16 |
case None => "" |
|
17 |
case Some(text) => " (" + text + ")" |
|
18 |
} |
|
74067 | 19 |
|
20 |
val interrupt_rc = 130 |
|
21 |
val timeout_rc = 142 |
|
22 |
||
71749 | 23 |
private val return_code_text = |
71748 | 24 |
Map(0 -> "OK", |
25 |
1 -> "ERROR", |
|
26 |
2 -> "FAILURE", |
|
72337 | 27 |
127 -> "COMMAND NOT FOUND", |
74067 | 28 |
interrupt_rc -> "INTERRUPT", |
71748 | 29 |
131 -> "QUIT SIGNAL", |
30 |
137 -> "KILL SIGNAL", |
|
31 |
138 -> "BUS ERROR", |
|
32 |
139 -> "SEGMENTATION VIOLATION", |
|
74067 | 33 |
timeout_rc -> "TIMEOUT", |
71748 | 34 |
143 -> "TERMINATION SIGNAL") |
71747 | 35 |
} |
36 |
||
62401 | 37 |
final case class Process_Result( |
62402 | 38 |
rc: Int, |
39 |
out_lines: List[String] = Nil, |
|
40 |
err_lines: List[String] = Nil, |
|
62569 | 41 |
timing: Timing = Timing.zero) |
62400 | 42 |
{ |
73277
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73134
diff
changeset
|
43 |
def out: String = Library.trim_line(cat_lines(out_lines)) |
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73134
diff
changeset
|
44 |
def err: String = Library.trim_line(cat_lines(err_lines)) |
71631 | 45 |
|
71646 | 46 |
def output(outs: List[String]): Process_Result = |
47 |
copy(out_lines = out_lines ::: outs.flatMap(split_lines)) |
|
48 |
def errors(errs: List[String]): Process_Result = |
|
49 |
copy(err_lines = err_lines ::: errs.flatMap(split_lines)) |
|
72002
5c4800f6b25a
more robust protocol for "Timing ..." messages, notably for pide_session=true;
wenzelm
parents:
71749
diff
changeset
|
50 |
def error(err: String): Process_Result = |
5c4800f6b25a
more robust protocol for "Timing ..." messages, notably for pide_session=true;
wenzelm
parents:
71749
diff
changeset
|
51 |
if (err.isEmpty) this else errors(List(err)) |
62400 | 52 |
|
53 |
def ok: Boolean = rc == 0 |
|
74067 | 54 |
def interrupted: Boolean = rc == Process_Result.interrupt_rc |
62400 | 55 |
|
73134
8a8ffe78eee7
clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents:
72726
diff
changeset
|
56 |
def timeout_rc: Process_Result = copy(rc = Process_Result.timeout_rc) |
8a8ffe78eee7
clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents:
72726
diff
changeset
|
57 |
def timeout: Boolean = rc == Process_Result.timeout_rc |
8a8ffe78eee7
clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents:
72726
diff
changeset
|
58 |
|
68927 | 59 |
def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1) |
60 |
||
72726
ec6a27bbdab8
proper return code for more errors (amending d892f6d66402);
wenzelm
parents:
72556
diff
changeset
|
61 |
def errors_rc(errs: List[String]): Process_Result = |
ec6a27bbdab8
proper return code for more errors (amending d892f6d66402);
wenzelm
parents:
72556
diff
changeset
|
62 |
if (errs.isEmpty) this else errors(errs).error_rc |
ec6a27bbdab8
proper return code for more errors (amending d892f6d66402);
wenzelm
parents:
72556
diff
changeset
|
63 |
|
64408
50bcf976f276
clarified hg push return code: 1 means "nothing to push";
wenzelm
parents:
64138
diff
changeset
|
64 |
def check_rc(pred: Int => Boolean): Process_Result = |
50bcf976f276
clarified hg push return code: 1 means "nothing to push";
wenzelm
parents:
64138
diff
changeset
|
65 |
if (pred(rc)) this |
62400 | 66 |
else if (interrupted) throw Exn.Interrupt() |
62492 | 67 |
else Exn.error(err) |
62400 | 68 |
|
64408
50bcf976f276
clarified hg push return code: 1 means "nothing to push";
wenzelm
parents:
64138
diff
changeset
|
69 |
def check: Process_Result = check_rc(_ == 0) |
50bcf976f276
clarified hg push return code: 1 means "nothing to push";
wenzelm
parents:
64138
diff
changeset
|
70 |
|
71747 | 71 |
def print_return_code: String = Process_Result.print_return_code(rc) |
72 |
def print_rc: String = Process_Result.print_rc(rc) |
|
73 |
||
62400 | 74 |
def print: Process_Result = |
75 |
{ |
|
64138
cf0c8c5782af
eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
wenzelm
parents:
64024
diff
changeset
|
76 |
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
|
77 |
Output.writeln(out) |
62404
13a0f537e232
retain tail out_lines as printed, but not the whole log content;
wenzelm
parents:
62402
diff
changeset
|
78 |
copy(out_lines = Nil, err_lines = Nil) |
62400 | 79 |
} |
62553 | 80 |
|
81 |
def print_stdout: Process_Result = |
|
82 |
{ |
|
64138
cf0c8c5782af
eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
wenzelm
parents:
64024
diff
changeset
|
83 |
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
|
84 |
Output.writeln(out, stdout = true) |
62553 | 85 |
copy(out_lines = Nil, err_lines = Nil) |
86 |
} |
|
62400 | 87 |
} |