# HG changeset patch
# User wenzelm
# Date 1406972353 -7200
# Node ID 074cb68b40a88149e13c5db814a32efce538aa2e
# Parent  d5b0fa6f1f7a81cd060d2888b1809c2da00c90f8
tuned output;

diff -r d5b0fa6f1f7a -r 074cb68b40a8 src/Pure/General/symbol.scala
--- 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] =