equal
deleted
inserted
replaced
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 object Process_Result |
9 object Process_Result |
10 { |
10 { |
11 def print_return_code(rc: Int): String = "Return code: " + rc |
11 val return_code_text: Map[Int, String] = |
|
12 Map(0 -> "OK", |
|
13 1 -> "ERROR", |
|
14 2 -> "FAILURE", |
|
15 130 -> "INTERRUPT", |
|
16 131 -> "QUIT SIGNAL", |
|
17 137 -> "KILL SIGNAL", |
|
18 138 -> "BUS ERROR", |
|
19 139 -> "SEGMENTATION VIOLATION", |
|
20 143 -> "TERMINATION SIGNAL") |
|
21 |
|
22 def print_return_code(rc: Int): String = |
|
23 { |
|
24 val text = return_code_text.get(rc) |
|
25 "Return code: " + rc + (if (text.isEmpty) "" else " (" + text.get + ")") |
|
26 } |
|
27 |
12 def print_rc(rc: Int): String = "return code " + rc |
28 def print_rc(rc: Int): String = "return code " + rc |
13 } |
29 } |
14 |
30 |
15 final case class Process_Result( |
31 final case class Process_Result( |
16 rc: Int, |
32 rc: Int, |