src/Pure/PIDE/document.ML
changeset 52586 7a0935571a23
parent 52573 815461c835b9
child 52587 067f1f950dc8
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 10 23:30:10 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 10:43:53 2013 +0200
     1.3 @@ -412,13 +412,9 @@
     1.4          let
     1.5            val flags' = update_flags prev flags;
     1.6            val same' =
     1.7 -            (case opt_exec of
     1.8 -              NONE => false
     1.9 -            | SOME (eval, _) =>
    1.10 -                (case lookup_entry node0 command_id of
    1.11 -                  NONE => false
    1.12 -                | SOME (eval0, _) =>
    1.13 -                    #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
    1.14 +            (case (lookup_entry node0 command_id, opt_exec) of
    1.15 +              (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval)
    1.16 +            | _ => false);
    1.17            val assign_update' = assign_update |>
    1.18              (case opt_exec of
    1.19                SOME (eval, prints) =>