src/Pure/PIDE/protocol.scala
changeset 66411 72de7d59e2f7
parent 66410 72a7e29104f1
child 66668 6019cfb8256c
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Aug 14 11:30:07 2017 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Aug 14 13:53:49 2017 +0200
     1.3 @@ -129,6 +129,7 @@
     1.4      unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
     1.5    {
     1.6      def total: Int = unprocessed + running + warned + failed + finished
     1.7 +    def ok: Boolean = failed == 0
     1.8    }
     1.9  
    1.10    def node_status(