print state only for visible command, to avoid wasting resources for the larger part of the text;
--- 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;