re-assign prints of unchanged eval only -- avoid crash of new_exec;
authorwenzelm
Thu, 11 Jul 2013 11:37:06 +0200
changeset 52588 bf90a4e842bc
parent 52587 067f1f950dc8
child 52589 d28d2d89034d
re-assign prints of unchanged eval only -- avoid crash of new_exec;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Jul 11 11:09:23 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 11 11:37:06 2013 +0200
@@ -415,7 +415,7 @@
             (case (lookup_entry node0 command_id, opt_exec) of
               (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval)
             | _ => false);
-          val assign_update' = assign_update |>
+          val assign_update' = assign_update |> same' ?
             (case opt_exec of
               SOME (eval, prints) =>
                 let