tuned output;
authorwenzelm
Wed, 26 Feb 2014 20:56:55 +0100
changeset 55777 90484dff4dc4
parent 55769 1f27d75ccf05
child 55778 e1fd8780f997
tuned output;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.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 + ")"
   }
 
 
--- 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 + ")"
   }