tuned output;

--- a/src/Pure/PIDE/document.scala	Fri Dec 01 20:41:59 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 01 20:49:42 2017 +0100
@@ -439,6 +439,8 @@
   final class History private(
     val undo_list: List[Change] = List(Change.init))  // non-empty list
   {
+    override def toString: String = "History(" + undo_list.length + ")"
+
     def tip: Change = undo_list.head
     def + (change: Change): History = new History(change :: undo_list)
 
@@ -569,6 +571,8 @@
       val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
       val is_finished: Boolean = false)
     {
+      override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")"
+
       def check_finished: Assignment = { require(is_finished); this }
       def unfinished: Assignment = new Assignment(command_execs, false)