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