src/Tools/jEdit/src/rendering.scala
changeset 55710 2d623ab55672
parent 55690 d73949233c2e
child 55713 734ac5709fbe
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 10:48:34 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 11:05:02 2014 +0100
     1.3 @@ -222,6 +222,9 @@
     1.4  
     1.5  class Rendering private(val snapshot: Document.Snapshot, val options: Options)
     1.6  {
     1.7 +  override def toString: String = "Rendering(" + snapshot.toString + ")"
     1.8 +
     1.9 +
    1.10    /* colors */
    1.11  
    1.12    def color_value(s: String): Color = Color_Value(options.string(s))