# HG changeset patch
# User wenzelm
# Date 1731848270 -3600
# Node ID a3dc66165d1546d97ccabd89a559d51ce93d25a0
# Parent  bb82ebb18b5dc3384ee72a5881cd07e57802b213
tuned;

diff -r bb82ebb18b5d -r a3dc66165d15 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 17 09:50:54 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 17 13:57:50 2024 +0100
@@ -335,26 +335,23 @@
 
     { (range: Text.Range) =>
       val stop = range.stop
+      try {
+        val p = text_area.offsetToXY(range.start)
+        val (q, r) =
+          if (get_text(buffer, Text.Range(stop - 1, stop)).contains("\n")) {
+            (text_area.offsetToXY(stop - 1), char_width)
+          }
+          else if (stop >= end) {
+            (text_area.offsetToXY(end), char_width * (stop - end))
+          }
+          else (text_area.offsetToXY(stop), 0)
 
-      val (p, q, r) =
-        try {
-          val p = text_area.offsetToXY(range.start)
-          val (q, r) =
-            if (get_text(buffer, Text.Range(stop - 1, stop)).contains("\n")) {
-              (text_area.offsetToXY(stop - 1), char_width)
-            }
-            else if (stop >= end) {
-              (text_area.offsetToXY(end), char_width * (stop - end))
-            }
-            else (text_area.offsetToXY(stop), 0)
-          (p, q, r)
+        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))
         }
-        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))
+        else None
       }
-      else None
+      catch { case _: ArrayIndexOutOfBoundsException => None }
     }
   }