src/Pure/PIDE/protocol.scala
changeset 66411 72de7d59e2f7
parent 66410 72a7e29104f1
child 66668 6019cfb8256c
--- 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(