author | wenzelm |
Wed, 30 Jun 2021 12:46:49 +0200 | |
changeset 73899 | 4d64bc387867 |
parent 73284 | a97ae083cad1 |
child 74142 | 0f051404f487 |
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 |
|
9 |
type T |
|
10 |
val make: |
|
11 |
{rc: int, |
|
12 |
out_lines: string list, |
|
13 |
err_lines: string list, |
|
14 |
timing: Timing.timing} -> T |
|
15 |
val rc: T -> int |
|
16 |
val out_lines: T -> string list |
|
17 |
val err_lines: T -> string list |
|
18 |
val timing: T -> Timing.timing |
|
73284 | 19 |
val timing_elapsed: T -> Time.time |
73275 | 20 |
val out: T -> string |
21 |
val err: T -> string |
|
22 |
val ok: T -> bool |
|
23 |
val check: T -> T |
|
73281 | 24 |
val print: T -> T |
73275 | 25 |
end; |
26 |
||
27 |
structure Process_Result: PROCESS_RESULT = |
|
28 |
struct |
|
29 |
||
30 |
abstype T = |
|
31 |
Process_Result of |
|
32 |
{rc: int, |
|
33 |
out_lines: string list, |
|
34 |
err_lines: string list, |
|
35 |
timing: Timing.timing} |
|
36 |
with |
|
37 |
||
38 |
val make = Process_Result; |
|
39 |
fun rep (Process_Result args) = args; |
|
40 |
||
41 |
val rc = #rc o rep; |
|
42 |
val out_lines = #out_lines o rep; |
|
43 |
val err_lines = #err_lines o rep; |
|
73284 | 44 |
|
73275 | 45 |
val timing = #timing o rep; |
73284 | 46 |
val timing_elapsed = #elapsed o timing; |
73275 | 47 |
|
73280 | 48 |
end; |
49 |
||
73277
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73275
diff
changeset
|
50 |
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
|
51 |
val err = trim_line o cat_lines o err_lines; |
73275 | 52 |
|
53 |
fun ok result = rc result = 0; |
|
54 |
||
73278
7dbae202ff84
clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;
wenzelm
parents:
73277
diff
changeset
|
55 |
fun check result = if ok result then result else error (err result); |
73275 | 56 |
|
73281 | 57 |
fun print result = |
58 |
(warning (err result); |
|
59 |
writeln (out result); |
|
60 |
make {rc = rc result, out_lines = [], err_lines = [], timing = timing result}); |
|
61 |
||
73275 | 62 |
end; |