src/Pure/PIDE/protocol.scala
changeset 50507 9605b0d93d1e
parent 50501 6f41f1646617
child 51293 05b1bbae748d
equal deleted inserted replaced
50505:33c92722cc3d 50507:9605b0d93d1e
   104       {
   104       {
   105         val st = state.command_state(version, command)
   105         val st = state.command_state(version, command)
   106         val status = command_status(st.status)
   106         val status = command_status(st.status)
   107         if (status.is_running) running += 1
   107         if (status.is_running) running += 1
   108         else if (status.is_finished) {
   108         else if (status.is_finished) {
   109           if (st.results.exists(p => is_warning(p._2))) warned += 1
   109           if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
   110           else finished += 1
   110           else finished += 1
   111         }
   111         }
   112         else if (status.is_failed) failed += 1
   112         else if (status.is_failed) failed += 1
   113         else unprocessed += 1
   113         else unprocessed += 1
   114       })
   114       })