proper priority for error over warning also for node_status (see 9c5220e05e04);
1.1 --- a/src/Pure/PIDE/protocol.scala Sat Aug 02 16:35:59 2014 +0200
1.2 +++ b/src/Pure/PIDE/protocol.scala Sat Aug 02 19:29:02 2014 +0200
1.3 @@ -145,8 +145,8 @@
1.4 val status = Status.merge(states.iterator.map(_.protocol_status))
1.5
1.6 if (status.is_running) running += 1
1.7 + else if (status.is_failed) failed += 1
1.8 else if (status.is_warned) warned += 1
1.9 - else if (status.is_failed) failed += 1
1.10 else if (status.is_finished) finished += 1
1.11 else unprocessed += 1
1.12 }