print state only for visible command, to avoid wasting resources for the larger part of the text;
authorwenzelm
Wed, 24 Aug 2011 13:40:10 +0200
changeset 44439 2bcd2aefaf7f
parent 44438 0fc38897248a
child 44440 aa2abd81f460
print state only for visible command, to avoid wasting resources for the larger part of the text;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Aug 24 13:38:07 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 24 13:40:10 2011 +0200
@@ -428,9 +428,8 @@
             let
               val (command_id, exec) = the_exec state exec_id;
               val (_, print) = Lazy.force exec;
-              val perspective = get_perspective node;
               val _ =
-                if #1 (get_perspective node) command_id orelse true  (* FIXME *)
+                if #1 (get_perspective node) command_id
                 then ignore (Lazy.future Future.default_params print)
                 else ();
             in () end;