diff -r d5f143b96334 -r f2db0596bd61 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 19 21:19:06 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 19 21:52:45 2012 +0200
@@ -168,5 +168,17 @@
       Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
     else None
   }
+
+
+  /* pixel range */
+
+  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
+  {
+    val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y))
+    gfx_range(text_area, range) match {
+      case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
+      case _ => None
+    }
+  }
 }