diff -r e6e5750f1311 -r 559b44b5164c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Apr 09 17:22:23 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Apr 09 17:38:39 2012 +0200
@@ -498,7 +498,7 @@
                     val (common, (visible, initial)) = last_common state last_visible node0 node;
                     val common_command_exec = the_default_entry node common;
 
-                    val (execs, (command_id, (_, exec)), _) =
+                    val (new_execs, (command_id', (_, exec')), _) =
                       ([], common_command_exec, if initial then SOME init else NONE) |>
                       (visible orelse required) ?
                         iterate_entries_after common
@@ -510,20 +510,20 @@
                       iterate_entries_after common
                         (fn ((_, id0), exec0) => fn res =>
                           if is_none exec0 then NONE
-                          else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
+                          else if exists (fn (_, (id, _)) => id0 = id) new_execs then SOME res
                           else SOME (id0 :: res)) node0 [];
 
-                    val last_exec = if command_id = no_id then NONE else SOME command_id;
+                    val last_exec = if command_id' = no_id then NONE else SOME command_id';
                     val result =
                       if is_some (after_entry node last_exec) then no_exec
-                      else exec;
+                      else exec';
 
                     val node' = node
                       |> fold reset_entry no_execs
-                      |> fold (fn (id, exec) => update_entry id (SOME exec)) execs
+                      |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
                       |> set_result result
                       |> set_touched false;
-                  in ((no_execs, execs, [(name, node')]), node') end)
+                  in ((no_execs, new_execs, [(name, node')]), node') end)
             end
           else Future.value (([], [], []), node))
       |> Future.joins |> map #1;