# 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) =>