diff -r b3a4207fb9a6 -r 47ed6a67a304 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