# 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 } } }