tuned signature;
authorwenzelm
Sun Nov 18 13:52:54 2012 +0100 (2012-11-18)
changeset 501158cde6f1a0106
parent 50114 d203e98ef5c9
child 50116 88b971fca902
tuned signature;
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 17 21:01:11 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 18 13:52:54 2012 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4  
     1.5    /* graphics range */
     1.6  
     1.7 -  class Gfx_Range(val x: Int, val y: Int, val length: Int)
     1.8 +  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
     1.9  
    1.10    // NB: jEdit always normalizes \r\n and \r to \n
    1.11    // NB: last line lacks \n
    1.12 @@ -165,7 +165,7 @@
    1.13        else (text_area.offsetToXY(stop), 0)
    1.14  
    1.15      if (p != null && q != null && p.x < q.x + r && p.y == q.y)
    1.16 -      Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
    1.17 +      Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
    1.18      else None
    1.19    }
    1.20