merged

--- 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)

--- 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 =