| author | wenzelm | 
| Sat, 08 Oct 2016 10:59:38 +0200 | |
| changeset 64098 | 099518e8af2c | 
| parent 64024 | 3dd92c391eca | 
| child 64138 | cf0c8c5782af | 
| 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, | |
| 62569 | 13 | timeout: Boolean = false, | 
| 14 | timing: Timing = Timing.zero) | |
| 62400 | 15 | {
 | 
| 16 | def out: String = cat_lines(out_lines) | |
| 17 | def err: String = cat_lines(err_lines) | |
| 62405 
d653532762e4
proper return code for timeout (amending f868f12f9419);
 wenzelm parents: 
62404diff
changeset | 18 | def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s)) | 
| 62400 | 19 | |
| 62569 | 20 | def was_timeout: Process_Result = copy(rc = 1, timeout = true) | 
| 62401 | 21 | |
| 62400 | 22 | def ok: Boolean = rc == 0 | 
| 23 | def interrupted: Boolean = rc == Exn.Interrupt.return_code | |
| 24 | ||
| 25 | def check: Process_Result = | |
| 26 | if (ok) this | |
| 27 | else if (interrupted) throw Exn.Interrupt() | |
| 62492 | 28 | else Exn.error(err) | 
| 62400 | 29 | |
| 30 | def print: Process_Result = | |
| 31 |   {
 | |
| 32 | Output.warning(Library.trim_line(err)) | |
| 33 | Output.writeln(Library.trim_line(out)) | |
| 62404 
13a0f537e232
retain tail out_lines as printed, but not the whole log content;
 wenzelm parents: 
62402diff
changeset | 34 | copy(out_lines = Nil, err_lines = Nil) | 
| 62400 | 35 | } | 
| 62553 | 36 | |
| 37 | def print_stdout: Process_Result = | |
| 38 |   {
 | |
| 39 | Output.warning(Library.trim_line(err), stdout = true) | |
| 40 | Output.writeln(Library.trim_line(out), stdout = true) | |
| 41 | copy(out_lines = Nil, err_lines = Nil) | |
| 42 | } | |
| 64024 | 43 | |
| 44 | def print_if(b: Boolean): Process_Result = if (b) print else this | |
| 45 | def print_stdout_if(b: Boolean): Process_Result = if (b) print_stdout else this | |
| 62400 | 46 | } |