# HG changeset patch
# User wenzelm
# Date 1385410638 -3600
# Node ID 7a8512d6206dfc0a52df53500ca2559a6d5d40a0
# Parent  2b38549374ba21ec1bbbc1e3c27ec7d1b5f3361f
more defensive order of Markup.failed vs. Markup.finished -- more informative status in Isabelle/Scala, although it is not rendered in Isabelle/jEdit;

diff -r 2b38549374ba -r 7a8512d6206d src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Nov 25 20:49:20 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Mon Nov 25 21:17:18 2013 +0100
@@ -165,18 +165,19 @@
       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;
-      val _ = Toplevel.status tr Markup.finished;
       val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
     in
       (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 _ = Toplevel.status tr Markup.failed;
           in {failed = true, malformed = malformed', command = tr, state = st} end
       | SOME st' =>
           let
             val _ = proof_status tr st';
+            val _ = Toplevel.status tr Markup.finished;
           in {failed = false, malformed = malformed', command = tr, state = st'} end)
     end;