src/Tools/jEdit/src/jedit_lib.scala
changeset 50116 88b971fca902
parent 50115 8cde6f1a0106
child 50186 f83cab68c788
equal deleted inserted replaced
50115:8cde6f1a0106 50116:88b971fca902
   172 
   172 
   173   /* pixel range */
   173   /* pixel range */
   174 
   174 
   175   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
   175   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
   176   {
   176   {
   177     val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y))
   177     val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y, false))
   178     gfx_range(text_area, range) match {
   178     gfx_range(text_area, range) match {
   179       case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
   179       case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
   180       case _ => None
   180       case _ => None
   181     }
   181     }
   182   }
   182   }