src/Pure/PIDE/document.ML
changeset 52596 40298d383463
parent 52595 76883c1e1c53
child 52599 d7871f38ffb4
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 12:28:24 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 14:42:11 2013 +0200
     1.3 @@ -421,7 +421,7 @@
     1.4            val flags' = update_flags prev flags;
     1.5            val same' =
     1.6              (case (lookup_entry node0 command_id, opt_exec) of
     1.7 -              (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval)
     1.8 +              (SOME (eval0, _), SOME (eval, _)) => Command.eval_same (eval0, eval)
     1.9              | _ => false);
    1.10            val assign_update' = assign_update |> same' ?
    1.11              (case opt_exec of