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)) }