# HG changeset patch # User wenzelm # Date 1393584654 -3600 # Node ID d3c9fa5206893359cf5f70a618d1b59de7c783c0 # Parent a1a8378bda422b2b2ccdf4564f59d095134aae40 tuned; diff -r a1a8378bda42 -r d3c9fa520689 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Feb 28 11:48:14 2014 +0100 +++ b/src/Pure/PIDE/document.scala Fri Feb 28 11:50:54 2014 +0100 @@ -24,8 +24,6 @@ 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) @@ -40,6 +38,8 @@ def remove(command: Command, fn: String, args: List[String]): Overlays = update(command.node_name, _.remove(command, fn, args)) + + override def toString: String = rep.mkString("Overlays(", ",", ")") } @@ -55,8 +55,6 @@ final class Blobs private(blobs: Map[Node.Name, Blob]) { - override def toString: String = blobs.mkString("Blobs(", ",", ")") - def get(name: Node.Name): Option[Blob] = blobs.get(name) def changed(name: Node.Name): Boolean = @@ -67,6 +65,8 @@ def retrieve(digest: SHA1.Digest): Option[Blob] = blobs.collectFirst({ case (_, blob) if blob.bytes.sha1_digest == digest => blob }) + + override def toString: String = blobs.mkString("Blobs(", ",", ")") } @@ -131,8 +131,6 @@ 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 @@ -140,6 +138,8 @@ new Overlays(rep.insert(cmd, (fn, args))) def remove(cmd: Command, fn: String, args: List[String]): Overlays = new Overlays(rep.remove(cmd, (fn, args))) + + override def toString: String = rep.mkString("Node.Overlays(", ",", ")") } @@ -665,10 +665,6 @@ (thy_load_commands zip other.thy_load_commands).forall(eq_commands) } - override def toString: String = - "Snapshot(node = " + node_name.node + ", version = " + version.id + - (if (is_outdated) ", outdated" else "") + ")" - /* cumulate markup */ @@ -727,6 +723,13 @@ for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status)) yield Text.Info(r, x) } + + + /* output */ + + override def toString: String = + "Snapshot(node = " + node_name.node + ", version = " + version.id + + (if (is_outdated) ", outdated" else "") + ")" } } }