# HG changeset patch
# User wenzelm
# Date 1535837444 -7200
# Node ID 13a984eba6125861a911dcd84ffe15984b4597ee
# Parent  cd7ab35aa40cdac7d289c56fd8deae00aef84c82
clarified message;

diff -r cd7ab35aa40c -r 13a984eba612 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sat Sep 01 20:25:53 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Sep 01 23:30:44 2018 +0200
@@ -232,14 +232,17 @@
       var ok = 0
       var failed = 0
       var pending = 0
+      var canceled = 0
       for (name <- rep.keysIterator) {
         overall_node_status(name) match {
           case Overall_Node_Status.ok => ok += 1
           case Overall_Node_Status.failed => failed += 1
           case Overall_Node_Status.pending => pending += 1
         }
+        if (apply(name).canceled) canceled += 1
       }
-      "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending + ")"
+      "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
+        ", canceled = " + canceled + ")"
     }
   }
 }