# HG changeset patch
# User wenzelm
# Date 1373386291 -7200
# Node ID 92ae3f0ca0603c1544b72b46b62fe132a7587e6a
# Parent  b6912471b8f509dd4984131bf10e966bb81fd4e0
tuned;

diff -r b6912471b8f5 -r 92ae3f0ca060 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Jul 09 18:08:56 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Jul 09 18:11:31 2013 +0200
@@ -438,10 +438,9 @@
         (_, node) <- version.nodes.entries
         command <- node.commands.iterator
       } {
-        val id = command.id
-        if (!commands1.isDefinedAt(id))
-          commands.get(id).foreach(st => commands1 += (id -> st))
-        for (exec_id <- command_execs.getOrElse(id, Nil)) {
+        if (!commands1.isDefinedAt(command.id))
+          commands.get(command.id).foreach(st => commands1 += (command.id -> st))
+        for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
           if (!execs1.isDefinedAt(exec_id))
             execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
         }