equal
deleted
inserted
replaced
|
1 /* Title: Pure/System/process_result.scala |
|
2 Author: Makarius |
|
3 |
|
4 Result of system process. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 final case class Process_Result(out_lines: List[String], err_lines: List[String], rc: Int) |
|
10 { |
|
11 def out: String = cat_lines(out_lines) |
|
12 def err: String = cat_lines(err_lines) |
|
13 |
|
14 def error(s: String, err_rc: Int = 0): Process_Result = |
|
15 copy(err_lines = err_lines ::: List(s), rc = rc max err_rc) |
|
16 |
|
17 def ok: Boolean = rc == 0 |
|
18 def interrupted: Boolean = rc == Exn.Interrupt.return_code |
|
19 |
|
20 def check: Process_Result = |
|
21 if (ok) this |
|
22 else if (interrupted) throw Exn.Interrupt() |
|
23 else Library.error(err) |
|
24 |
|
25 def print: Process_Result = |
|
26 { |
|
27 Output.warning(Library.trim_line(err)) |
|
28 Output.writeln(Library.trim_line(out)) |
|
29 Process_Result(Nil, Nil, rc) |
|
30 } |
|
31 } |