equal
deleted
inserted
replaced
304 fun debugging f x = |
304 fun debugging f x = |
305 if ! debug then exception_trace (fn () => f x) |
305 if ! debug then exception_trace (fn () => f x) |
306 else f x; |
306 else f x; |
307 |
307 |
308 fun interruptible f x = |
308 fun interruptible f x = |
309 let val y = ref x |
309 let val y = ref NONE |
310 in raise_interrupt (fn () => y := f x) (); ! y end; |
310 in raise_interrupt (fn () => y := SOME (f x)) (); the (! y) end; |
311 |
311 |
312 fun toplevel_error f x = f x |
312 fun toplevel_error f x = f x |
313 handle exn => (Output.error_msg (exn_message exn); raise TOPLEVEL_ERROR); |
313 handle exn => (Output.error_msg (exn_message exn); raise TOPLEVEL_ERROR); |
314 |
314 |
315 in |
315 in |
399 |
399 |
400 fun undo_limit int = if int then NONE else SOME 0; |
400 fun undo_limit int = if int then NONE else SOME 0; |
401 |
401 |
402 fun safe_exit (Toplevel (SOME (node, (exit, _)))) = |
402 fun safe_exit (Toplevel (SOME (node, (exit, _)))) = |
403 (case try the_global_theory (History.current node) of |
403 (case try the_global_theory (History.current node) of |
404 SOME thy => exit thy |
404 SOME thy => controlled_execution exit thy |
405 | NONE => ()) |
405 | NONE => ()) |
406 | safe_exit _ = (); |
406 | safe_exit _ = (); |
407 |
407 |
408 local |
408 local |
409 |
409 |