--- 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 */
--- 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))