# HG changeset patch
# User wenzelm
# Date 1530002977 -7200
# Node ID f483fe1813f0c5959eb6311af8dd39f1c6af9ed7
# Parent  71483c0e0023089728572c8a3a99d956b253c884# Parent  7266fb64de69617b7c45064a8e1f8e9421165fd4
merged

diff -r 71483c0e0023 -r f483fe1813f0 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Mon Jun 25 17:18:59 2018 +0200
+++ b/src/Pure/General/graph.scala	Tue Jun 26 10:49:37 2018 +0200
@@ -68,6 +68,7 @@
   def defined(x: Key): Boolean = rep.isDefinedAt(x)
   def domain: Set[Key] = rep.keySet
 
+  def size: Int = rep.size
   def iterator: Iterator[(Key, Entry)] = rep.iterator
 
   def keys_iterator: Iterator[Key] = iterator.map(_._1)
diff -r 71483c0e0023 -r f483fe1813f0 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Jun 25 17:18:59 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Jun 26 10:49:37 2018 +0200
@@ -669,6 +669,16 @@
     /*intermediate state between remove_versions/removed_versions*/
     removing_versions: Boolean = false)
   {
+    override def toString: String =
+      "State(versions = " + versions.size +
+      ", blobs = " + blobs.size +
+      ", commands = " + commands.size +
+      ", execs = " + execs.size +
+      ", assignments = " + assignments.size +
+      ", commands_redirection = " + commands_redirection.size +
+      ", history = " + history.undo_list.size +
+      ", removing_versions = " + removing_versions + ")"
+
     private def fail[A]: A = throw new State.Fail(this)
 
     def define_version(version: Version, assignment: State.Assignment): State =