src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Thu Feb 27 12:37:43 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Feb 27 12:48:59 2014 +0100
@@ -24,6 +24,8 @@
 
   final class Overlays private(rep: Map[Node.Name, Node.Overlays])
   {
+    override def toString: String = rep.mkString("Overlays(", ",", ")")
+
     def apply(name: Document.Node.Name): Node.Overlays =
       rep.getOrElse(name, Node.Overlays.empty)
 
@@ -104,6 +106,8 @@
 
     final class Overlays private(rep: Multi_Map[Command, (String, List[String])])
     {
+      override def toString: String = rep.mkString("Node.Overlays(", ",", ")")
+
       def commands: Set[Command] = rep.keySet
       def is_empty: Boolean = rep.isEmpty
       def dest: List[(Command, (String, List[String]))] = rep.iterator.toList