# HG changeset patch
# User wenzelm
# Date 1695123971 -7200
# Node ID 90b12b919b5f7dbc9125a67d2ef7d066a85a5b62
# Parent  fcdfd3251892d6b593c246b048e7b3d3d85aab7a
clarified signature (again): follow Isabelle/Java/Scala;

diff -r fcdfd3251892 -r 90b12b919b5f src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Tue Sep 19 13:12:13 2023 +0200
+++ b/src/Pure/General/exn.ML	Tue Sep 19 13:46:11 2023 +0200
@@ -30,6 +30,7 @@
   val interrupt_exn: 'a result
   val is_interrupt_exn: 'a result -> bool
   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+  val failure_rc: exn -> int
   exception EXCEPTIONS of exn list
   val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
 end;
@@ -99,6 +100,8 @@
 fun interruptible_capture f x =
   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
+fun failure_rc exn = if is_interrupt exn then 130 else 2;
+
 
 (* concatenated exceptions *)
 
diff -r fcdfd3251892 -r 90b12b919b5f src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Tue Sep 19 13:12:13 2023 +0200
+++ b/src/Pure/System/command_line.ML	Tue Sep 19 13:46:11 2023 +0200
@@ -15,11 +15,9 @@
 fun tool body =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
-      fun return_code exn =
-        if Exn.is_interrupt exn then 130 else 2;
       val rc =
         (restore_attributes body (); 0) handle exn =>
-          ((Runtime.exn_error_message exn; return_code exn) handle err => return_code err);
+          ((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err);
     in exit rc end) ();
 
 end;