# HG changeset patch
# User wenzelm
# Date 1373535426 -7200
# Node ID bf90a4e842bc35d8e7449d309ea7dced9cf41984
# Parent  067f1f950dc89ca0efe2ab71857d45ffbf7c5ce4
re-assign prints of unchanged eval only -- avoid crash of new_exec;

diff -r 067f1f950dc8 -r bf90a4e842bc 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