src/Tools/jEdit/src/jedit_lib.scala

   }
 
 
   /* 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
   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   {

       else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
         (text_area.offsetToXY(stop - 1), char_width(text_area))
       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
   }
 
 
   /* pixel range */