run commands as interactive, again after long history of fluctuation (9e196062bf88, 173974e07dea, e07dacec79e7) and quite different infrastructure for print tasks;
authorwenzelm
Wed, 07 May 2014 13:25:54 +0200
changeset 56896 1e3c3df3a77c
parent 56895 f058120aaad4
child 56897 c668735fb8b5
run commands as interactive, again after long history of fluctuation (9e196062bf88, 173974e07dea, e07dacec79e7) and quite different infrastructure for print tasks;
src/Pure/PIDE/command.ML
--- 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;