# HG changeset patch
# User wenzelm
# Date 1314186010 -7200
# Node ID 2bcd2aefaf7f054b3d39736b31d47ee196c815cb
# Parent  0fc38897248a46103079b2f493467e8f63550b65
print state only for visible command, to avoid wasting resources for the larger part of the text;

diff -r 0fc38897248a -r 2bcd2aefaf7f 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;