# HG changeset patch
# User wenzelm
# Date 1205273370 -3600
# Node ID 707969e76f5c1616a1ef30104a0e241c203c8d17
# Parent  3e7939e978c67085e553de5864ad41f914811ce9
raw_loop: more graceful crash recovery;

diff -r 3e7939e978c6 -r 707969e76f5c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Mar 11 22:31:09 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Mar 11 23:09:30 2008 +0100
@@ -772,8 +772,9 @@
       NONE => (writeln "\nInterrupt."; raw_loop secure src)
     | SOME NONE => if secure then quit () else ()
     | SOME (SOME (tr, src')) => if >> tr orelse check_secure () then raw_loop secure src' else ())
-    handle exn => (CRITICAL (fn () => change crashes (cons exn));
-      warning "Recovering after Isar toplevel crash -- see also Toplevel.crashes";
+    handle exn => (Output.error_msg (exn_message exn) handle crash =>
+      (CRITICAL (fn () => change crashes (cons crash));
+        warning "Recovering after Isar toplevel crash -- see also Toplevel.crashes");
       raw_loop secure src)
   end;