diff -r 72a7e29104f1 -r 72de7d59e2f7 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Aug 14 11:30:07 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Aug 14 13:53:49 2017 +0200
@@ -129,6 +129,7 @@
     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
   {
     def total: Int = unprocessed + running + warned + failed + finished
+    def ok: Boolean = failed == 0
   }
 
   def node_status(