src/Pure/PIDE/document.scala
changeset 55800 d3c9fa520689
parent 55783 da0513d95155
child 55801 28b59620f0d0
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Feb 28 11:48:14 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Feb 28 11:50:54 2014 +0100
     1.3 @@ -24,8 +24,6 @@
     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 @@ -40,6 +38,8 @@
    1.13  
    1.14      def remove(command: Command, fn: String, args: List[String]): Overlays =
    1.15        update(command.node_name, _.remove(command, fn, args))
    1.16 +
    1.17 +    override def toString: String = rep.mkString("Overlays(", ",", ")")
    1.18    }
    1.19  
    1.20  
    1.21 @@ -55,8 +55,6 @@
    1.22  
    1.23    final class Blobs private(blobs: Map[Node.Name, Blob])
    1.24    {
    1.25 -    override def toString: String = blobs.mkString("Blobs(", ",", ")")
    1.26 -
    1.27      def get(name: Node.Name): Option[Blob] = blobs.get(name)
    1.28  
    1.29      def changed(name: Node.Name): Boolean =
    1.30 @@ -67,6 +65,8 @@
    1.31  
    1.32      def retrieve(digest: SHA1.Digest): Option[Blob] =
    1.33        blobs.collectFirst({ case (_, blob) if blob.bytes.sha1_digest == digest => blob })
    1.34 +
    1.35 +    override def toString: String = blobs.mkString("Blobs(", ",", ")")
    1.36    }
    1.37  
    1.38  
    1.39 @@ -131,8 +131,6 @@
    1.40  
    1.41      final class Overlays private(rep: Multi_Map[Command, (String, List[String])])
    1.42      {
    1.43 -      override def toString: String = rep.mkString("Node.Overlays(", ",", ")")
    1.44 -
    1.45        def commands: Set[Command] = rep.keySet
    1.46        def is_empty: Boolean = rep.isEmpty
    1.47        def dest: List[(Command, (String, List[String]))] = rep.iterator.toList
    1.48 @@ -140,6 +138,8 @@
    1.49          new Overlays(rep.insert(cmd, (fn, args)))
    1.50        def remove(cmd: Command, fn: String, args: List[String]): Overlays =
    1.51          new Overlays(rep.remove(cmd, (fn, args)))
    1.52 +
    1.53 +      override def toString: String = rep.mkString("Node.Overlays(", ",", ")")
    1.54      }
    1.55  
    1.56  
    1.57 @@ -665,10 +665,6 @@
    1.58            (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
    1.59          }
    1.60  
    1.61 -        override def toString: String =
    1.62 -          "Snapshot(node = " + node_name.node + ", version = " + version.id +
    1.63 -            (if (is_outdated) ", outdated" else "") + ")"
    1.64 -
    1.65  
    1.66          /* cumulate markup */
    1.67  
    1.68 @@ -727,6 +723,13 @@
    1.69            for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status))
    1.70              yield Text.Info(r, x)
    1.71          }
    1.72 +
    1.73 +
    1.74 +        /* output */
    1.75 +
    1.76 +        override def toString: String =
    1.77 +          "Snapshot(node = " + node_name.node + ", version = " + version.id +
    1.78 +            (if (is_outdated) ", outdated" else "") + ")"
    1.79        }
    1.80      }
    1.81    }