safe_exit: controlled_execution;

--- a/src/Pure/Isar/toplevel.ML	Sat Oct 27 18:37:33 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Oct 28 11:57:04 2007 +0100
@@ -306,8 +306,8 @@
   else f x;
 
 fun interruptible f x =
-  let val y = ref x
-  in raise_interrupt (fn () => y := f x) (); ! y end;
+  let val y = ref NONE
+  in raise_interrupt (fn () => y := SOME (f x)) (); the (! y) end;
 
 fun toplevel_error f x = f x
   handle exn => (Output.error_msg (exn_message exn); raise TOPLEVEL_ERROR);
@@ -401,7 +401,7 @@
 
 fun safe_exit (Toplevel (SOME (node, (exit, _)))) =
     (case try the_global_theory (History.current node) of
-      SOME thy => exit thy
+      SOME thy => controlled_execution exit thy
     | NONE => ())
   | safe_exit _ = ();