more robust: avoid spurious crash of text_area.getText() in Active_Area.update();
authorwenzelm
Wed, 11 Dec 2024 12:03:01 +0100
changeset 81580 2e7073976c25
parent 81579 cf4bebd770b5
child 81581 8a3608933607
more robust: avoid spurious crash of text_area.getText() in Active_Area.update();
src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Dec 11 11:18:52 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Dec 11 12:03:01 2024 +0100
@@ -365,12 +365,14 @@
   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] = {
     // coordinates wrt. inner painter component
     val painter = text_area.getPainter
+    val buffer = text_area.getBuffer
     if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
       val offset = text_area.xyToOffset(x, y, false)
       if (offset >= 0) {
-        val range = point_range(text_area.getBuffer, offset)
+        val range = point_range(buffer, offset)
         gfx_range(text_area)(range) match {
-          case Some(g) if g.x <= x && x < g.x + g.length => Some(range)
+          case Some(g) if g.x <= x && x < g.x + g.length =>
+            range.try_restrict(buffer_range(buffer))
           case _ => None
         }
       }