author | wenzelm |
Thu, 11 Jul 2013 11:37:06 +0200 | |
changeset 52588 | bf90a4e842bc |
parent 52587 | 067f1f950dc8 |
child 52589 | d28d2d89034d |
--- 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