# 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