# HG changeset patch
# User wenzelm
# Date 1534596801 -7200
# Node ID be5f255a9943c5aae5cef5460d4694abc62e4461
# Parent  b523e903d6e408a6171e6319954492ebddb021ea
tuned output;

diff -r b523e903d6e4 -r be5f255a9943 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 14:42:42 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 14:53:21 2018 +0200
@@ -212,6 +212,20 @@
         case other: Nodes_Status => rep == other.rep
         case _ => false
       }
-    override def toString: String = rep.iterator.mkString("Nodes_Status(", ", ", ")")
+
+    override def toString: String =
+    {
+      var ok = 0
+      var failed = 0
+      var pending = 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
+        }
+      }
+      "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending + ")"
+    }
   }
 }