src/Tools/jEdit/src/jedit_lib.scala
changeset 49941 f2db0596bd61
parent 49843 afddf4e26fac
child 50115 8cde6f1a0106
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 19 21:19:06 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 19 21:52:45 2012 +0200
     1.3 @@ -168,5 +168,17 @@
     1.4        Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
     1.5      else None
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* pixel range */
    1.10 +
    1.11 +  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
    1.12 +  {
    1.13 +    val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y))
    1.14 +    gfx_range(text_area, range) match {
    1.15 +      case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
    1.16 +      case _ => None
    1.17 +    }
    1.18 +  }
    1.19  }
    1.20