tuned;
authorwenzelm
Tue, 06 Jan 2009 21:17:37 +0100
changeset 29370 98aaf2cd873f
parent 29369 393f72663b49
child 29375 68b453811232
tuned;
src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Tue Jan 06 14:45:45 2009 +0100
+++ b/src/Pure/Isar/isar.ML	Tue Jan 06 21:17:37 2009 +0100
@@ -133,11 +133,12 @@
     (case Source.get_single (Source.set_prompt Source.default_prompt src) of
       NONE => if secure then quit () else ()
     | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
-    handle exn => (Output.error_msg (Toplevel.exn_message exn)
-    handle crash =>
-      (CRITICAL (fn () => change crashes (cons crash));
-        warning "Recovering after Isar toplevel crash -- see also Isar.crashes");
-      raw_loop secure src)
+    handle exn =>
+      (Output.error_msg (Toplevel.exn_message exn)
+        handle crash =>
+          (CRITICAL (fn () => change crashes (cons crash));
+            warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
+          raw_loop secure src)
   end;
 
 in