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