# HG changeset patch
# User wenzelm
# Date 1586792444 -7200
# Node ID 77232ff6b8f6928f559a99c538f228072763a2d8
# Parent  34de8369c2902360968643eed297d73eec6c09e5
tuned message;
tuned signature;

diff -r 34de8369c290 -r 77232ff6b8f6 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Mon Apr 13 16:32:56 2020 +0200
+++ b/src/Pure/System/process_result.scala	Mon Apr 13 17:40:44 2020 +0200
@@ -8,7 +8,15 @@
 
 object Process_Result
 {
-  val return_code_text: Map[Int, String] =
+  def print_return_code(rc: Int): String = "Return code: " + rc + rc_text(rc)
+  def print_rc(rc: Int): String = "return code " + rc + rc_text(rc)
+
+  def rc_text(rc: Int): String =
+    return_code_text.get(rc) match {
+      case None => ""
+      case Some(text) => " (" + text + ")"
+    }
+  private val return_code_text =
     Map(0 -> "OK",
       1 -> "ERROR",
       2 -> "FAILURE",
@@ -18,14 +26,6 @@
       138 -> "BUS ERROR",
       139 -> "SEGMENTATION VIOLATION",
       143 -> "TERMINATION SIGNAL")
-
-  def print_return_code(rc: Int): String =
-  {
-    val text = return_code_text.get(rc)
-    "Return code: " + rc + (if (text.isEmpty) "" else " (" + text.get + ")")
-  }
-
-  def print_rc(rc: Int): String = "return code " + rc
 }
 
 final case class Process_Result(