# HG changeset patch
# User wenzelm
# Date 1236801243 -3600
# Node ID c999618d225e376e5f7cb11c4563da74d5ced972
# Parent  52361140a0d150da206360315ef2ae3f8be8c1e4
debugging: special handling of EXCURSION_FAIL;

diff -r 52361140a0d1 -r c999618d225e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Mar 11 20:42:16 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 11 20:54:03 2009 +0100
@@ -294,9 +294,10 @@
 
 fun debugging f x =
   if ! debug then
-    (case exception_trace (fn () => SOME (f x) handle UNDEF => NONE) of
-      SOME y => y
-    | NONE => raise UNDEF)
+    Exn.release (exception_trace (fn () =>
+      Exn.Result (f x) handle
+        exn as UNDEF => Exn.Exn exn
+      | exn as EXCURSION_FAIL _ => Exn.Exn exn))
   else f x;
 
 fun toplevel_error f x =