clarified message;
authorwenzelm
Sat Sep 01 23:30:44 2018 +0200 (11 months ago)
changeset 6887313a984eba612
parent 68872 cd7ab35aa40c
child 68874 cca5ca811714
clarified message;
src/Pure/PIDE/document_status.scala
     1.1 --- a/src/Pure/PIDE/document_status.scala	Sat Sep 01 20:25:53 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document_status.scala	Sat Sep 01 23:30:44 2018 +0200
     1.3 @@ -232,14 +232,17 @@
     1.4        var ok = 0
     1.5        var failed = 0
     1.6        var pending = 0
     1.7 +      var canceled = 0
     1.8        for (name <- rep.keysIterator) {
     1.9          overall_node_status(name) match {
    1.10            case Overall_Node_Status.ok => ok += 1
    1.11            case Overall_Node_Status.failed => failed += 1
    1.12            case Overall_Node_Status.pending => pending += 1
    1.13          }
    1.14 +        if (apply(name).canceled) canceled += 1
    1.15        }
    1.16 -      "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending + ")"
    1.17 +      "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
    1.18 +        ", canceled = " + canceled + ")"
    1.19      }
    1.20    }
    1.21  }