# HG changeset patch
# User wenzelm
# Date 1393236302 -3600
# Node ID 2d623ab55672979c711ac38785edb07115046176
# Parent  4e5a83a46ded44d54269bc170b8a80d971001298
tuned messages;

diff -r 4e5a83a46ded -r 2d623ab55672 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Feb 24 10:48:34 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Feb 24 11:05:02 2014 +0100
@@ -634,6 +634,10 @@
           (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 */
 
diff -r 4e5a83a46ded -r 2d623ab55672 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 10:48:34 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 11:05:02 2014 +0100
@@ -222,6 +222,9 @@
 
 class Rendering private(val snapshot: Document.Snapshot, val options: Options)
 {
+  override def toString: String = "Rendering(" + snapshot.toString + ")"
+
+
   /* colors */
 
   def color_value(s: String): Color = Color_Value(options.string(s))