equal
deleted
inserted
replaced
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 } |