# HG changeset patch
# User wenzelm
# Date 1283871088 -7200
# Node ID ed394608635865833e044185c545ff67deb8b24e
# Parent  31b95e0da7b742a8958dbdc6ba6402f6f5b36f40
Command.State.accumulate: check actual source range;

diff -r 31b95e0da7b7 -r ed3946086358 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Sep 07 16:40:30 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 07 16:51:28 2010 +0200
@@ -48,11 +48,11 @@
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
           (this /: msgs)((state, msg) =>
             msg match {
-              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
-              if id == command.id =>
+              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
+              if id == command.id && command.range.contains(command.decode(raw_range)) =>
+                val range = command.decode(raw_range)
                 val props = Position.purge(atts)
-                val info =
-                  Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
+                val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
                 state.add_markup(info)
               case _ => System.err.println("Ignored report message: " + msg); state
             })