# HG changeset patch
# User wenzelm
# Date 1535921691 -7200
# Node ID 1167f2d8a167804d75b3aa07a9e684210286b1cc
# Parent  17486b8218e22e3a9c8fb48785300f6e7a894820
more robust: avoid race-condition of terminated vs. consolidated;

diff -r 17486b8218e2 -r 1167f2d8a167 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Sep 02 22:34:50 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Sun Sep 02 22:54:51 2018 +0200
@@ -268,11 +268,11 @@
         in {failed = true, command = tr, state = st} end
     | SOME st' =>
         let
-          val _ = status tr Markup.finished;
           val _ =
             if Keyword.is_theory_end keywords (Toplevel.name_of tr) andalso
               can (Toplevel.end_theory Position.none) st'
             then status tr Markup.finalized else ();
+          val _ = status tr Markup.finished;
         in {failed = false, command = tr, state = st'} end)
   end;