# HG changeset patch
# User wenzelm
# Date 1393444615 -3600
# Node ID 90484dff4dc40b5f804ae7372ed054b4d674da84
# Parent  1f27d75ccf05171ea8a853e60e50a8b045d63ce3
tuned output;

diff -r 1f27d75ccf05 -r 90484dff4dc4 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Feb 26 17:14:23 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Feb 26 20:56:55 2014 +0100
@@ -228,6 +228,8 @@
     val range = Text.Range(0, length)
     private val symbol_index = Symbol.Index(text)
     def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
+
+    override def toString: String = "Command.File(" + file_name + ")"
   }
 
 
diff -r 1f27d75ccf05 -r 90484dff4dc4 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Feb 26 17:14:23 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Feb 26 20:56:55 2014 +0100
@@ -292,6 +292,8 @@
     val nodes: Nodes = Nodes.empty)
   {
     def is_init: Boolean = id == Document_ID.none
+
+    override def toString: String = "Version(" + id + ")"
   }