src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Wed Apr 09 09:37:49 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Apr 09 10:44:06 2014 +0200
@@ -688,7 +688,7 @@
           } yield (id, st)).toMap.valuesIterator.toList
         }
         else Nil
-      self.map(_._2) ::: others.map(_.redirect(command))
+      self.map(_._2) ::: others.flatMap(_.redirect(command))
     }
 
     def command_results(version: Version, command: Command): Command.Results =