# HG changeset patch
# User wenzelm
# Date 1353243174 -3600
# Node ID 8cde6f1a0106a21fd94a46837264226bc1721e2e
# Parent  d203e98ef5c945f13d97eca80d4ff61491f20746
tuned signature;

diff -r d203e98ef5c9 -r 8cde6f1a0106 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 17 21:01:11 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 18 13:52:54 2012 +0100
@@ -146,7 +146,7 @@
 
   /* graphics range */
 
-  class Gfx_Range(val x: Int, val y: Int, val length: Int)
+  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
 
   // NB: jEdit always normalizes \r\n and \r to \n
   // NB: last line lacks \n
@@ -165,7 +165,7 @@
       else (text_area.offsetToXY(stop), 0)
 
     if (p != null && q != null && p.x < q.x + r && p.y == q.y)
-      Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
+      Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
     else None
   }