|
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 |
|
19 val out: T -> string |
|
20 val err: T -> string |
|
21 val ok: T -> bool |
|
22 val interrupted: T -> bool |
|
23 val check_rc: (int -> bool) -> T -> T |
|
24 val check: T -> T |
|
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; |
|
44 val timing = #timing o rep; |
|
45 |
|
46 val out = cat_lines o out_lines; |
|
47 val err = cat_lines o err_lines; |
|
48 |
|
49 fun ok result = rc result = 0; |
|
50 fun interrupted result = rc result = Exn.interrupt_return_code; |
|
51 |
|
52 fun check_rc pred result = |
|
53 if pred (rc result) then result |
|
54 else if interrupted result then raise Exn.Interrupt |
|
55 else error (err result); |
|
56 |
|
57 val check = check_rc (fn rc => rc = 0); |
|
58 |
|
59 end; |
|
60 |
|
61 end; |