src/Pure/PIDE/document.ML
changeset 44439 2bcd2aefaf7f
parent 44436 546adfa8a6fc
child 44440 aa2abd81f460
equal deleted inserted replaced
44438:0fc38897248a 44439:2bcd2aefaf7f
   426       fun force_exec _ NONE = ()
   426       fun force_exec _ NONE = ()
   427         | force_exec node (SOME exec_id) =
   427         | force_exec node (SOME exec_id) =
   428             let
   428             let
   429               val (command_id, exec) = the_exec state exec_id;
   429               val (command_id, exec) = the_exec state exec_id;
   430               val (_, print) = Lazy.force exec;
   430               val (_, print) = Lazy.force exec;
   431               val perspective = get_perspective node;
       
   432               val _ =
   431               val _ =
   433                 if #1 (get_perspective node) command_id orelse true  (* FIXME *)
   432                 if #1 (get_perspective node) command_id
   434                 then ignore (Lazy.future Future.default_params print)
   433                 then ignore (Lazy.future Future.default_params print)
   435                 else ();
   434                 else ();
   436             in () end;
   435             in () end;
   437 
   436 
   438       val execution = Future.new_group NONE;
   437       val execution = Future.new_group NONE;