changeset 44439 | 2bcd2aefaf7f |
parent 44436 | 546adfa8a6fc |
child 44440 | aa2abd81f460 |
--- 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;