src/Pure/Isar/toplevel.ML

   val debug: bool ref
   val interact: bool ref
   val timing: bool ref
   val profiling: int ref
   val skip_proofs: bool ref
+  val crashes: exn list ref
   exception TERMINATE
   exception RESTART
   exception TOPLEVEL_ERROR
   val exn_message: exn -> string
   val program: (unit -> 'a) -> 'a

 val debug = Output.debugging;
 val interact = ref false;
 val timing = Output.timing;
 val profiling = ref 0;
 val skip_proofs = ref false;
+val crashes = ref ([]: exn list);
 
 exception TERMINATE;
 exception RESTART;
 exception EXCURSION_FAIL of exn * string;
 exception FAILURE of state * exn;

   in
     (case get_interrupt (Source.set_prompt prompt src) of
       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";
+      raw_loop secure src)
   end;
 
 in
 
 fun loop secure src = ignore_interrupt (raw_loop secure) src;