# HG changeset patch
# User wenzelm
# Date 1231273057 -3600
# Node ID 98aaf2cd873fe884c4ee10230053cdf47051c458
# Parent  393f72663b497498b1718de787da6f9be30804c9
tuned;

diff -r 393f72663b49 -r 98aaf2cd873f 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