# HG changeset patch
# User wenzelm
# Date 1399461954 -7200
# Node ID 1e3c3df3a77cedabcdc6f5082978c36c88e46fe8
# Parent  f058120aaad4fe7cf3be741dec73d2c640cf940b
run commands as interactive, again after long history of fluctuation (9e196062bf88, 173974e07dea, e07dacec79e7) and quite different infrastructure for print tasks;

diff -r f058120aaad4 -r 1e3c3df3a77c 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;