src/Pure/PIDE/document.ML
changeset 52607 33a133d50616
parent 52606 0d68d108d7e0
child 52655 3b2b1ef13979
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 12 11:28:03 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 12 12:04:16 2013 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  
     1.5  fun changed_result node node' =
     1.6    (case (get_result node, get_result node') of
     1.7 -    (SOME eval, SOME eval') => not (Command.eval_same (eval, eval'))
     1.8 +    (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval'))
     1.9    | (NONE, NONE) => false
    1.10    | _ => true);
    1.11  
    1.12 @@ -401,7 +401,8 @@
    1.13            val flags' = update_flags prev flags;
    1.14            val same' =
    1.15              (case (lookup_entry node0 command_id, opt_exec) of
    1.16 -              (SOME (eval0, _), SOME (eval, _)) => Command.eval_same (eval0, eval)
    1.17 +              (SOME (eval0, _), SOME (eval, _)) =>
    1.18 +                Command.eval_eq (eval0, eval) andalso Command.eval_stable eval
    1.19              | _ => false);
    1.20            val assign_update' = assign_update |> same' ?
    1.21              (case opt_exec of
    1.22 @@ -445,7 +446,7 @@
    1.23  
    1.24  fun cancel_old_execs node0 (command_id, exec_ids) =
    1.25    subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
    1.26 -  |> map_filter (Execution.peek_running #> Option.map (tap Future.cancel_group));
    1.27 +  |> map_filter (Execution.peek #> Option.map (tap Future.cancel_group));
    1.28  
    1.29  in
    1.30