1.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 10 23:30:10 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 11 10:43:53 2013 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val exec_ids: exec option -> Document_ID.exec list
     1.5    val stable_eval: eval -> bool
     1.6    val stable_print: print -> bool
     1.7 +  val same_eval: eval * eval -> bool
     1.8    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
     1.9    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.10    val print: bool -> string -> eval -> print list -> print list option
    1.11 @@ -111,6 +112,9 @@
    1.12  fun stable_print ({exec_id, print_process, ...}: print) =
    1.13    stable_goals exec_id andalso memo_stable print_process;
    1.14  
    1.15 +fun same_eval (eval: eval, eval': eval) =
    1.16 +  #exec_id eval = #exec_id eval' andalso stable_eval eval';
    1.17 +
    1.18  
    1.19  (* read *)
    1.20  

     2.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 10 23:30:10 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 10:43:53 2013 +0200
     2.3 @@ -412,13 +412,9 @@
     2.4          let
     2.5            val flags' = update_flags prev flags;
     2.6            val same' =
     2.7 -            (case opt_exec of
     2.8 -              NONE => false
     2.9 -            | SOME (eval, _) =>
    2.10 -                (case lookup_entry node0 command_id of
    2.11 -                  NONE => false
    2.12 -                | SOME (eval0, _) =>
    2.13 -                    #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
    2.14 +            (case (lookup_entry node0 command_id, opt_exec) of
    2.15 +              (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval)
    2.16 +            | _ => false);
    2.17            val assign_update' = assign_update |>
    2.18              (case opt_exec of
    2.19                SOME (eval, prints) =>