author | wenzelm |
Mon, 07 Mar 2016 20:44:47 +0100 | |
changeset 62548 | f8ebb715e06d |
parent 62492 | 0e53fade87fe |
child 62553 | d2e0d626fb96 |
permissions | -rw-r--r-- |
62400 | 1 |
/* Title: Pure/System/process_result.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Result of system process. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
62401 | 9 |
final case class Process_Result( |
62402 | 10 |
rc: Int, |
11 |
out_lines: List[String] = Nil, |
|
12 |
err_lines: List[String] = Nil, |
|
13 |
timeout: Option[Time] = None) |
|
62400 | 14 |
{ |
15 |
def out: String = cat_lines(out_lines) |
|
16 |
def err: String = cat_lines(err_lines) |
|
62405
d653532762e4
proper return code for timeout (amending f868f12f9419);
wenzelm
parents:
62404
diff
changeset
|
17 |
def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s)) |
62400 | 18 |
|
62405
d653532762e4
proper return code for timeout (amending f868f12f9419);
wenzelm
parents:
62404
diff
changeset
|
19 |
def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t)) |
62401 | 20 |
|
62400 | 21 |
def ok: Boolean = rc == 0 |
22 |
def interrupted: Boolean = rc == Exn.Interrupt.return_code |
|
23 |
||
24 |
def check: Process_Result = |
|
25 |
if (ok) this |
|
26 |
else if (interrupted) throw Exn.Interrupt() |
|
62492 | 27 |
else Exn.error(err) |
62400 | 28 |
|
29 |
def print: Process_Result = |
|
30 |
{ |
|
31 |
Output.warning(Library.trim_line(err)) |
|
32 |
Output.writeln(Library.trim_line(out)) |
|
62404
13a0f537e232
retain tail out_lines as printed, but not the whole log content;
wenzelm
parents:
62402
diff
changeset
|
33 |
copy(out_lines = Nil, err_lines = Nil) |
62400 | 34 |
} |
35 |
} |