# HG changeset patch
# User wenzelm
# Date 1360181106 -3600
# Node ID 4e1c940b1fb255cdfee4755b63e5f3f995cbd838
# Parent  ea0cb5ff5ae7a1158587510a8414c92c5ae1e8ad
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;

diff -r ea0cb5ff5ae7 -r 4e1c940b1fb2 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Feb 06 20:03:42 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Feb 06 21:05:06 2013 +0100
@@ -172,15 +172,20 @@
 
     val buffer = text_area.getBuffer
 
-    val p = text_area.offsetToXY(range.start)
-
     val end = buffer.getLength
     val stop = range.stop
-    val (q, r) =
-      if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
-      else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
-        (text_area.offsetToXY(stop - 1), char_width)
-      else (text_area.offsetToXY(stop), 0)
+
+    val (p, q, r) =
+      try {
+        val p = text_area.offsetToXY(range.start)
+        val (q, r) =
+          if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
+          else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
+            (text_area.offsetToXY(stop - 1), char_width)
+          else (text_area.offsetToXY(stop), 0)
+        (p, q, r)
+      }
+      catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
 
     if (p != null && q != null && p.x < q.x + r && p.y == q.y)
       Some(Gfx_Range(p.x, p.y, q.x + r - p.x))