# HG changeset patch
# User wenzelm
# Date 1695121368 -7200
# Node ID 66e7a3131fe34173a15aae88d82e2cfc452cf85c
# Parent  f8595f6d39a59336ca4644c57b985f51f8ef0816
tuned --- avoid pointless indirection (see also a2df9de46060);

diff -r f8595f6d39a5 -r 66e7a3131fe3 src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/Pure/General/exn.ML	Tue Sep 19 13:02:48 2023 +0200
@@ -30,8 +30,6 @@
   val interrupt_exn: 'a result
   val is_interrupt_exn: 'a result -> bool
   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
-  val return_code: exn -> int -> int
-  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
   exception EXCEPTIONS of exn list
   val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
 end;
@@ -102,15 +100,6 @@
   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
 
-(* POSIX return code *)
-
-fun return_code exn rc =
-  if is_interrupt exn then 130 else rc;
-
-fun capture_exit rc f x =
-  f x handle exn => exit (return_code exn rc);
-
-
 (* concatenated exceptions *)
 
 exception EXCEPTIONS of exn list;
diff -r f8595f6d39a5 -r 66e7a3131fe3 src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/Pure/System/command_line.ML	Tue Sep 19 13:02:48 2023 +0200
@@ -15,9 +15,11 @@
 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 => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
+        (restore_attributes body (); 0) handle exn =>
+          ((Runtime.exn_error_message exn; return_code exn) handle err => return_code err);
     in exit rc end) ();
 
 end;