46 }) |
46 }) |
47 |
47 |
48 case XML.Elem(Markup(Markup.REPORT, _), msgs) => |
48 case XML.Elem(Markup(Markup.REPORT, _), msgs) => |
49 (this /: msgs)((state, msg) => |
49 (this /: msgs)((state, msg) => |
50 msg match { |
50 msg match { |
51 case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args) |
51 case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args) |
52 if id == command.id => |
52 if id == command.id && command.range.contains(command.decode(raw_range)) => |
|
53 val range = command.decode(raw_range) |
53 val props = Position.purge(atts) |
54 val props = Position.purge(atts) |
54 val info = |
55 val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args)) |
55 Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args)) |
|
56 state.add_markup(info) |
56 state.add_markup(info) |
57 case _ => System.err.println("Ignored report message: " + msg); state |
57 case _ => System.err.println("Ignored report message: " + msg); state |
58 }) |
58 }) |
59 case XML.Elem(Markup(name, atts), body) => |
59 case XML.Elem(Markup(name, atts), body) => |
60 atts match { |
60 atts match { |