tuned signature: more operations;

--- a/src/Pure/System/process_result.scala	Sun Jul 23 18:39:23 2023 +0200
+++ b/src/Pure/System/process_result.scala	Sun Jul 23 19:20:29 2023 +0200
@@ -47,14 +47,13 @@
 
     def merge(rcs: IterableOnce[Int]): Int = rcs.iterator.foldLeft(ok)(merge)
 
+    def apply(ok: Boolean): Int = if (ok) RC.ok else RC.error
+    def apply(exn: Throwable): Int = if (Exn.is_interrupt(exn)) interrupt else error
     def apply(result: Exn.Result[Process_Result]): Int =
       result match {
         case Exn.Res(res) => res.rc
-        case Exn.Exn(Exn.Interrupt()) => interrupt
-        case Exn.Exn(_) => error
+        case Exn.Exn(exn) => apply(exn)
       }
-
-    def apply(ok: Boolean): Int = if (ok) RC.ok else RC.error
   }
 
   val undefined: Process_Result = Process_Result(RC.undefined)