--- a/src/Pure/PIDE/command.ML Thu Aug 30 22:38:12 2012 +0200
+++ b/src/Pure/PIDE/command.ML Fri Aug 31 13:23:25 2012 +0200
@@ -105,13 +105,13 @@
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
@@ -122,7 +122,6 @@
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