equal
deleted
inserted
replaced
291 (* controlled execution *) |
291 (* controlled execution *) |
292 |
292 |
293 local |
293 local |
294 |
294 |
295 fun debugging f x = |
295 fun debugging f x = |
296 if ! debug then exception_trace (fn () => f x) |
296 if ! debug then |
|
297 (case exception_trace (fn () => SOME (f x) handle UNDEF => NONE) of |
|
298 SOME y => y |
|
299 | NONE => raise UNDEF) |
297 else f x; |
300 else f x; |
298 |
301 |
299 fun toplevel_error f x = |
302 fun toplevel_error f x = |
300 let val ctxt = try ML_Context.the_local_context () in |
303 let val ctxt = try ML_Context.the_local_context () in |
301 f x handle exn => |
304 f x handle exn => |