src/Pure/PIDE/document.scala
changeset 55782 47ed6a67a304
parent 55777 90484dff4dc4
child 55783 da0513d95155
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Feb 27 12:37:43 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Feb 27 12:48:59 2014 +0100
     1.3 @@ -24,6 +24,8 @@
     1.4  
     1.5    final class Overlays private(rep: Map[Node.Name, Node.Overlays])
     1.6    {
     1.7 +    override def toString: String = rep.mkString("Overlays(", ",", ")")
     1.8 +
     1.9      def apply(name: Document.Node.Name): Node.Overlays =
    1.10        rep.getOrElse(name, Node.Overlays.empty)
    1.11  
    1.12 @@ -104,6 +106,8 @@
    1.13  
    1.14      final class Overlays private(rep: Multi_Map[Command, (String, List[String])])
    1.15      {
    1.16 +      override def toString: String = rep.mkString("Node.Overlays(", ",", ")")
    1.17 +
    1.18        def commands: Set[Command] = rep.keySet
    1.19        def is_empty: Boolean = rep.isEmpty
    1.20        def dest: List[(Command, (String, List[String]))] = rep.iterator.toList