src/Pure/PIDE/command.ML

       val malformed' = Toplevel.is_malformed tr;
       val is_init = Toplevel.is_init tr;
       val is_proof = Keyword.is_proof (Toplevel.name_of tr);
 
       val _ = Multithreading.interrupted ();
-      val _ = Toplevel.status tr Isabelle_Markup.forked;
+      val _ = Toplevel.status tr Isabelle_Markup.running;
       val start = Timing.start ();
       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 tr cmts st');
       val errs = errs1 @ errs2;
       val _ = timing tr (Timing.result start);
-      val _ = Toplevel.status tr Isabelle_Markup.joined;
+      val _ = Toplevel.status tr Isabelle_Markup.finished;
       val _ = List.app (Toplevel.error_msg tr) errs;
     in
       (case result of
         NONE =>
           let
             val _ = if null errs then Exn.interrupt () else ();
             val _ = Toplevel.status tr Isabelle_Markup.failed;
           in ((st, malformed'), no_print) end
       | SOME st' =>
           let
-            val _ = Toplevel.status tr Isabelle_Markup.finished;
             val _ = proof_status tr st';
             val do_print =
               not is_init andalso
                 (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
           in ((st', malformed'), if do_print then print_state tr st' else no_print) end)