# HG changeset patch
# User wenzelm
# Date 1373532233 -7200
# Node ID 7a0935571a23bf82a78c9f88f264913c609e01e0
# Parent  ff525a38dba90bc91004c685d132a427adfde570
tuned;

diff -r ff525a38dba9 -r 7a0935571a23 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Jul 10 23:30:10 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Jul 11 10:43:53 2013 +0200
@@ -18,6 +18,7 @@
   val exec_ids: exec option -> Document_ID.exec list
   val stable_eval: eval -> bool
   val stable_print: print -> bool
+  val same_eval: eval * eval -> bool
   val read: (unit -> theory) -> Token.T list -> Toplevel.transition
   val eval: (unit -> theory) -> Token.T list -> eval -> eval
   val print: bool -> string -> eval -> print list -> print list option
@@ -111,6 +112,9 @@
 fun stable_print ({exec_id, print_process, ...}: print) =
   stable_goals exec_id andalso memo_stable print_process;
 
+fun same_eval (eval: eval, eval': eval) =
+  #exec_id eval = #exec_id eval' andalso stable_eval eval';
+
 
 (* read *)
 
diff -r ff525a38dba9 -r 7a0935571a23 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Jul 10 23:30:10 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 11 10:43:53 2013 +0200
@@ -412,13 +412,9 @@
         let
           val flags' = update_flags prev flags;
           val same' =
-            (case opt_exec of
-              NONE => false
-            | SOME (eval, _) =>
-                (case lookup_entry node0 command_id of
-                  NONE => false
-                | SOME (eval0, _) =>
-                    #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
+            (case (lookup_entry node0 command_id, opt_exec) of
+              (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval)
+            | _ => false);
           val assign_update' = assign_update |>
             (case opt_exec of
               SOME (eval, prints) =>