Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
simplified Toplevel.error_msg;

--- a/src/Pure/Isar/toplevel.ML	Mon Aug 30 15:19:39 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Aug 30 16:49:41 2010 +0200
@@ -84,7 +84,7 @@
   val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val status: transition -> Markup.T -> unit
-  val error_msg: transition -> exn * string -> unit
+  val error_msg: transition -> string -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val run_command: string -> transition -> state -> state option
@@ -563,9 +563,8 @@
 fun status tr m =
   setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
 
-fun error_msg tr exn_info =
-  setmp_thread_position tr (fn () =>
-    Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
+fun error_msg tr msg =
+  setmp_thread_position tr (fn () => Output.error_msg msg) ();
 
 
 (* post-transition hooks *)
@@ -623,6 +622,11 @@
 
 local
 
+fun proof_status tr st =
+  (case try proof_of st of
+    SOME prf => status tr (Proof.status_markup prf)
+  | NONE => ());
+
 fun async_state (tr as Transition {print, ...}) st =
   if print then
     ignore
@@ -630,11 +634,6 @@
           setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
   else ();
 
-fun proof_status tr st =
-  (case try proof_of st of
-    SOME prf => status tr (Proof.status_markup prf)
-  | NONE => ());
-
 in
 
 fun run_command thy_name tr st =
@@ -643,18 +642,28 @@
         SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
       | NONE => Exn.Result ()) of
     Exn.Result () =>
-      let val int = is_some (init_of tr) in
-        (case transition int tr st of
-          SOME (st', NONE) =>
-           (status tr Markup.finished;
-            proof_status tr st';
-            if int then () else async_state tr st';
-            SOME st')
-        | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
-        | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
-        | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
-      end
-  | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
+      let
+        val int = is_some (init_of tr);
+        val (errs, result) =
+          (case transition int tr st of
+            SOME (st', NONE) => ([], SOME st')
+          | SOME (_, SOME exn_info) =>
+              (case ML_Compiler.exn_messages (EXCURSION_FAIL exn_info) of
+                [] => raise Exn.Interrupt
+              | errs => (errs, NONE))
+          | NONE => ([ML_Compiler.exn_message TERMINATE], NONE));
+        val _ = List.app (error_msg tr) errs;
+        val _ =
+          (case result of
+            NONE => status tr Markup.failed
+          | SOME st' =>
+             (status tr Markup.finished;
+              proof_status tr st';
+              if int then () else async_state tr st'));
+      in result end
+  | Exn.Exn exn =>
+     (error_msg tr (ML_Compiler.exn_message (EXCURSION_FAIL (exn, at_command tr)));
+      status tr Markup.failed; NONE))
 
 end;
 

--- a/src/Pure/System/isar.ML	Mon Aug 30 15:19:39 2010 +0200
+++ b/src/Pure/System/isar.ML	Mon Aug 30 16:49:41 2010 +0200
@@ -94,7 +94,10 @@
 fun op >> tr =
   (case Toplevel.transition true tr (state ()) of
     NONE => false
-  | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
+  | SOME (_, SOME exn_info) =>
+     (set_exn (SOME exn_info);
+      Toplevel.error_msg tr (ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+      true)
   | SOME (st', NONE) =>
       let
         val name = Toplevel.name_of tr;