author | wenzelm |
Sat, 07 Aug 2021 22:23:37 +0200 | |
changeset 74142 | 0f051404f487 |
parent 73284 | a97ae083cad1 |
permissions | -rw-r--r-- |
73275 | 1 |
(* Title: Pure/System/process_result.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Result of system process. |
|
5 |
*) |
|
6 |
||
7 |
signature PROCESS_RESULT = |
|
8 |
sig |
|
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
73284
diff
changeset
|
9 |
val interrupt_rc: int |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
73284
diff
changeset
|
10 |
val timeout_rc: int |
73275 | 11 |
type T |
12 |
val make: |
|
13 |
{rc: int, |
|
14 |
out_lines: string list, |
|
15 |
err_lines: string list, |
|
16 |
timing: Timing.timing} -> T |
|
17 |
val rc: T -> int |
|
18 |
val out_lines: T -> string list |
|
19 |
val err_lines: T -> string list |
|
20 |
val timing: T -> Timing.timing |
|
73284 | 21 |
val timing_elapsed: T -> Time.time |
73275 | 22 |
val out: T -> string |
23 |
val err: T -> string |
|
24 |
val ok: T -> bool |
|
25 |
val check: T -> T |
|
73281 | 26 |
val print: T -> T |
73275 | 27 |
end; |
28 |
||
29 |
structure Process_Result: PROCESS_RESULT = |
|
30 |
struct |
|
31 |
||
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
73284
diff
changeset
|
32 |
val interrupt_rc = 130 |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
73284
diff
changeset
|
33 |
val timeout_rc = 142 |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
73284
diff
changeset
|
34 |
|
73275 | 35 |
abstype T = |
36 |
Process_Result of |
|
37 |
{rc: int, |
|
38 |
out_lines: string list, |
|
39 |
err_lines: string list, |
|
40 |
timing: Timing.timing} |
|
41 |
with |
|
42 |
||
43 |
val make = Process_Result; |
|
44 |
fun rep (Process_Result args) = args; |
|
45 |
||
46 |
val rc = #rc o rep; |
|
47 |
val out_lines = #out_lines o rep; |
|
48 |
val err_lines = #err_lines o rep; |
|
73284 | 49 |
|
73275 | 50 |
val timing = #timing o rep; |
73284 | 51 |
val timing_elapsed = #elapsed o timing; |
73275 | 52 |
|
73280 | 53 |
end; |
54 |
||
73277
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73275
diff
changeset
|
55 |
val out = trim_line o cat_lines o out_lines; |
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73275
diff
changeset
|
56 |
val err = trim_line o cat_lines o err_lines; |
73275 | 57 |
|
58 |
fun ok result = rc result = 0; |
|
59 |
||
73278
7dbae202ff84
clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;
wenzelm
parents:
73277
diff
changeset
|
60 |
fun check result = if ok result then result else error (err result); |
73275 | 61 |
|
73281 | 62 |
fun print result = |
63 |
(warning (err result); |
|
64 |
writeln (out result); |
|
65 |
make {rc = rc result, out_lines = [], err_lines = [], timing = timing result}); |
|
66 |
||
73275 | 67 |
end; |