tuned output;

--- a/src/Pure/General/symbol.scala	Fri Aug 01 22:52:53 2014 +0200
+++ b/src/Pure/General/symbol.scala	Sat Aug 02 11:39:13 2014 +0200
@@ -203,6 +203,8 @@
         case _ => false
       }
 
+    override def toString: String = "Text_Chunk" + range.toString
+
     def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset)
     def decode(symbol_range: Range): Text.Range = index.decode(symbol_range)
     def incorporate(symbol_range: Range): Option[Text.Range] =