# HG changeset patch
# User wenzelm
# Date 1398160385 -7200
# Node ID a2df9de46060b271dd15dfaa1e42ed58d05bb514
# Parent  cb912b7de3cfda02befe662749e7995818588612
tuned -- avoid warning about catch-all handler;

diff -r cb912b7de3cf -r a2df9de46060 bin/isabelle_process
--- a/bin/isabelle_process	Tue Apr 22 11:47:57 2014 +0200
+++ b/bin/isabelle_process	Tue Apr 22 11:53:05 2014 +0200
@@ -223,7 +223,7 @@
   "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
     fail "Failed to retrieve Isabelle system options"
   if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
-    MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
+    MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
   fi
   if [ -n "$PROOFGENERAL" ]; then
     MLTEXT="$MLTEXT; ProofGeneral.init ();"
diff -r cb912b7de3cf -r a2df9de46060 src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Tue Apr 22 11:47:57 2014 +0200
+++ b/src/Pure/General/exn.ML	Tue Apr 22 11:53:05 2014 +0200
@@ -19,6 +19,7 @@
   val interrupt_exn: 'a result
   val is_interrupt_exn: 'a result -> bool
   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
   exception EXCEPTIONS of exn list
 end;
 
@@ -67,6 +68,12 @@
   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
 
+(* POSIX process wrapper *)
+
+fun capture_exit rc f x =
+  f x handle exn => if is_interrupt exn then exit (130: int) else exit rc;
+
+
 (* concatenated exceptions *)
 
 exception EXCEPTIONS of exn list;
diff -r cb912b7de3cf -r a2df9de46060 src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Tue Apr 22 11:47:57 2014 +0200
+++ b/src/Pure/System/command_line.ML	Tue Apr 22 11:53:05 2014 +0200
@@ -15,13 +15,10 @@
 
 fun tool body =
   uninterruptible (fn restore_attributes => fn () =>
-    let val rc =
-      restore_attributes body () handle exn =>
-        let
-          val _ =
-            Runtime.exn_error_message exn
-              handle _ => Output.error_message "Exception raised, but failed to print details!";
-        in if Exn.is_interrupt exn then 130 else 1 end;
+    let
+      val rc =
+        restore_attributes body () handle exn =>
+          Exn.capture_exit 1 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
     in if rc = 0 then () else exit rc end) ();
 
 fun tool0 body = tool (fn () => (body (); 0));