equal
deleted
inserted
replaced
4 Result of system process. |
4 Result of system process. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 object Process_Result |
9 object Process_Result { |
10 { |
|
11 /* return code */ |
10 /* return code */ |
12 |
11 |
13 object RC |
12 object RC { |
14 { |
|
15 val ok = 0 |
13 val ok = 0 |
16 val error = 1 |
14 val error = 1 |
17 val failure = 2 |
15 val failure = 2 |
18 val interrupt = 130 |
16 val interrupt = 130 |
19 val timeout = 142 |
17 val timeout = 142 |
20 |
18 |
21 private def text(rc: Int): String = |
19 private def text(rc: Int): String = { |
22 { |
|
23 val txt = |
20 val txt = |
24 rc match { |
21 rc match { |
25 case `ok` => "OK" |
22 case `ok` => "OK" |
26 case `error` => "ERROR" |
23 case `error` => "ERROR" |
27 case `failure` => "FAILURE" |
24 case `failure` => "FAILURE" |
45 |
42 |
46 final case class Process_Result( |
43 final case class Process_Result( |
47 rc: Int, |
44 rc: Int, |
48 out_lines: List[String] = Nil, |
45 out_lines: List[String] = Nil, |
49 err_lines: List[String] = Nil, |
46 err_lines: List[String] = Nil, |
50 timing: Timing = Timing.zero) |
47 timing: Timing = Timing.zero |
51 { |
48 ) { |
52 def out: String = Library.trim_line(cat_lines(out_lines)) |
49 def out: String = Library.trim_line(cat_lines(out_lines)) |
53 def err: String = Library.trim_line(cat_lines(err_lines)) |
50 def err: String = Library.trim_line(cat_lines(err_lines)) |
54 |
51 |
55 def output(outs: List[String]): Process_Result = |
52 def output(outs: List[String]): Process_Result = |
56 copy(out_lines = out_lines ::: outs.flatMap(split_lines)) |
53 copy(out_lines = out_lines ::: outs.flatMap(split_lines)) |
79 def check: Process_Result = check_rc(_ == Process_Result.RC.ok) |
76 def check: Process_Result = check_rc(_ == Process_Result.RC.ok) |
80 |
77 |
81 def print_return_code: String = Process_Result.RC.print_long(rc) |
78 def print_return_code: String = Process_Result.RC.print_long(rc) |
82 def print_rc: String = Process_Result.RC.print(rc) |
79 def print_rc: String = Process_Result.RC.print(rc) |
83 |
80 |
84 def print: Process_Result = |
81 def print: Process_Result = { |
85 { |
|
86 Output.warning(err) |
82 Output.warning(err) |
87 Output.writeln(out) |
83 Output.writeln(out) |
88 copy(out_lines = Nil, err_lines = Nil) |
84 copy(out_lines = Nil, err_lines = Nil) |
89 } |
85 } |
90 |
86 |
91 def print_stdout: Process_Result = |
87 def print_stdout: Process_Result = { |
92 { |
|
93 Output.warning(err, stdout = true) |
88 Output.warning(err, stdout = true) |
94 Output.writeln(out, stdout = true) |
89 Output.writeln(out, stdout = true) |
95 copy(out_lines = Nil, err_lines = Nil) |
90 copy(out_lines = Nil, err_lines = Nil) |
96 } |
91 } |
97 } |
92 } |