tuned output;
authorwenzelm
Wed Feb 26 20:56:55 2014 +0100 (2014-02-26)
changeset 5577790484dff4dc4
parent 55769 1f27d75ccf05
child 55778 e1fd8780f997
tuned output;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Feb 26 17:14:23 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Feb 26 20:56:55 2014 +0100
     1.3 @@ -228,6 +228,8 @@
     1.4      val range = Text.Range(0, length)
     1.5      private val symbol_index = Symbol.Index(text)
     1.6      def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
     1.7 +
     1.8 +    override def toString: String = "Command.File(" + file_name + ")"
     1.9    }
    1.10  
    1.11  
     2.1 --- a/src/Pure/PIDE/document.scala	Wed Feb 26 17:14:23 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Wed Feb 26 20:56:55 2014 +0100
     2.3 @@ -292,6 +292,8 @@
     2.4      val nodes: Nodes = Nodes.empty)
     2.5    {
     2.6      def is_init: Boolean = id == Document_ID.none
     2.7 +
     2.8 +    override def toString: String = "Version(" + id + ")"
     2.9    }
    2.10  
    2.11