# HG changeset patch
# User wenzelm
# Date 1733914981 -3600
# Node ID 2e7073976c252a25ded1263ade88eb488fd1ab9a
# Parent  cf4bebd770b5842bf6fa11364c058a4baed01638
more robust: avoid spurious crash of text_area.getText() in Active_Area.update();

diff -r cf4bebd770b5 -r 2e7073976c25 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
         }
       }