changeset 37044 | d93b849cbecd |
parent 36735 | 42b7f881f5fc |
child 37072 | 9105c8237c7a |
--- a/src/Pure/PIDE/state.scala Fri May 21 18:10:19 2010 +0200 +++ b/src/Pure/PIDE/state.scala Fri May 21 20:10:45 2010 +0200 @@ -74,7 +74,7 @@ { val changed: State = message match { - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => + case XML.Elem(Markup.STATUS, _, elems) => (this /: elems)((state, elem) => elem match { case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)