# HG changeset patch
# User wenzelm
# Date 1236717799 -3600
# Node ID 9e9b8adddb9342a4ec74d8c138da21cd21d0a1ba
# Parent  9498e99e58a66f6a6aa6594d2f5e1c2f6ef474eb
controlled_execution/debugging: special handling of UNDEF to prevent it to appear in exception_trace;

diff -r 9498e99e58a6 -r 9e9b8adddb93 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Mar 10 21:20:01 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Mar 10 21:43:19 2009 +0100
@@ -293,7 +293,10 @@
 local
 
 fun debugging f x =
-  if ! debug then exception_trace (fn () => f x)
+  if ! debug then
+    (case exception_trace (fn () => SOME (f x) handle UNDEF => NONE) of
+      SOME y => y
+    | NONE => raise UNDEF)
   else f x;
 
 fun toplevel_error f x =