--- a/src/Pure/PIDE/command.ML Wed May 07 12:59:15 2014 +0200
+++ b/src/Pure/PIDE/command.ML Wed May 07 13:25:54 2014 +0200
@@ -226,12 +226,10 @@
else
let
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 _ = status tr Markup.running;
- val (errs1, result) = run (is_init orelse is_proof) tr st;
+ val (errs1, result) = run true tr st;
val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
val errs = errs1 @ errs2;
val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;