# HG changeset patch
# User wenzelm
# Date 1386271373 -3600
# Node ID 87910da843d507259e229e02b9660bc92e426db8
# Parent  ae5426994961e9060ec955cd83a383e48596cfeb
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
tuned signature;

diff -r ae5426994961 -r 87910da843d5 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Dec 05 20:06:28 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 05 20:22:53 2013 +0100
@@ -88,7 +88,6 @@
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
-  val status: transition -> Markup.T -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
   val get_timing: transition -> Time.time option
   val put_timing: Time.time option -> transition -> transition
@@ -586,9 +585,6 @@
 fun setmp_thread_position (Transition {pos, ...}) f x =
   Position.setmp_thread_data pos f x;
 
-fun status tr m =
-  setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
-
 
 (* post-transition hooks *)
 
diff -r ae5426994961 -r 87910da843d5 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Dec 05 20:06:28 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Dec 05 20:22:53 2013 +0100
@@ -179,9 +179,15 @@
             if Exn.is_interrupt exn then reraise exn
             else ML_Compiler.exn_messages_ids exn)) ();
 
+fun report tr m =
+  Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) ();
+
+fun status tr m =
+  Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
+
 fun proof_status tr st =
   (case try Toplevel.proof_of st of
-    SOME prf => Toplevel.status tr (Proof.status_markup prf)
+    SOME prf => status tr (Proof.status_markup prf)
   | NONE => ());
 
 fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
@@ -194,7 +200,7 @@
       val is_proof = Keyword.is_proof (Toplevel.name_of tr);
 
       val _ = Multithreading.interrupted ();
-      val _ = Toplevel.status tr Markup.running;
+      val _ = status tr Markup.running;
       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
       val errs = errs1 @ errs2;
@@ -203,14 +209,14 @@
       (case result of
         NONE =>
           let
-            val _ = Toplevel.status tr Markup.failed;
-            val _ = Toplevel.status tr Markup.finished;
-            val _ = if null errs then Exn.interrupt () else ();
+            val _ = status tr Markup.failed;
+            val _ = status tr Markup.finished;
+            val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
           in {failed = true, malformed = malformed', command = tr, state = st} end
       | SOME st' =>
           let
             val _ = proof_status tr st';
-            val _ = Toplevel.status tr Markup.finished;
+            val _ = status tr Markup.finished;
           in {failed = false, malformed = malformed', command = tr, state = st'} end)
     end;
 
diff -r ae5426994961 -r 87910da843d5 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Thu Dec 05 20:06:28 2013 +0100
+++ b/src/Pure/PIDE/execution.ML	Thu Dec 05 20:22:53 2013 +0100
@@ -107,13 +107,14 @@
               val _ = status task [Markup.joined];
               val _ =
                 (case result of
-                  Exn.Res _ => ()
-                | Exn.Exn exn =>
+                  Exn.Exn exn =>
                    (status task [Markup.failed];
+                    status task [Markup.finished];
                     Output.report (Markup.markup_only Markup.bad);
                     if exec_id = 0 then ()
-                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
-              val _ = status task [Markup.finished];
+                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))
+                | Exn.Res _ =>
+                    status task [Markup.finished])
             in Exn.release result end);
 
       val _ = status (Future.task_of future) [Markup.forked];