changeset 30422 | 9e9b8adddb93 |
parent 30398 | d7ac4b7aa590 |
child 30460 | c999618d225e |
--- 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 =