diff -r 33c92722cc3d -r 9605b0d93d1e src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu Dec 13 19:53:55 2012 +0100 +++ b/src/Pure/PIDE/protocol.scala Fri Dec 14 12:09:08 2012 +0100 @@ -106,7 +106,7 @@ val status = command_status(st.status) if (status.is_running) running += 1 else if (status.is_finished) { - if (st.results.exists(p => is_warning(p._2))) warned += 1 + if (st.results.entries.exists(p => is_warning(p._2))) warned += 1 else finished += 1 } else if (status.is_failed) failed += 1