# HG changeset patch # User wenzelm # Date 1731783270 -3600 # Node ID dc35aa7d5311781e52b72c4362101febf8b5363b # Parent b82ee80baa0534e8bef0e81c65bc70e8f43bf6f6 minor performance tuning: avoided repeated metric initialization; diff -r b82ee80baa05 -r dc35aa7d5311 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Sat Nov 16 19:07:24 2024 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Sat Nov 16 19:54:30 2024 +0100 @@ -326,34 +326,36 @@ // NB: jEdit always normalizes \r\n and \r to \n // NB: last line lacks \n - def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = { + def gfx_range(text_area: TextArea): Text.Range => Option[Gfx_Range] = { val metric = font_metric(text_area.getPainter) val char_width = metric.average_width.round.toInt val buffer = text_area.getBuffer + val end = buffer.getLength - val end = buffer.getLength - val stop = range.stop + { (range: Text.Range) => + val stop = range.stop - 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) + 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) + } + 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)) } - 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 } @@ -366,7 +368,7 @@ val offset = text_area.xyToOffset(x, y, false) if (offset >= 0) { val range = point_range(text_area.getBuffer, offset) - gfx_range(text_area, range) match { + gfx_range(text_area)(range) match { case Some(g) if g.x <= x && x < g.x + g.length => Some(range) case _ => None } diff -r b82ee80baa05 -r dc35aa7d5311 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Sat Nov 16 19:07:24 2024 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Nov 16 19:54:30 2024 +0100 @@ -98,6 +98,7 @@ @volatile private var painter_rendering: JEdit_Rendering = null @volatile private var painter_clip: Shape = null + @volatile private var painter_gfx_range: Text.Range => Option[JEdit_Lib.Gfx_Range] = null @volatile private var caret_focus = Rendering.Focus.empty private val set_state = new TextAreaExtension { @@ -113,6 +114,7 @@ ): Unit = { painter_rendering = get_rendering() painter_clip = gfx.getClip + painter_gfx_range = JEdit_Lib.gfx_range(text_area) caret_focus = if (caret_enabled && !painter_rendering.snapshot.is_outdated) { painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), caret_focus_range) @@ -134,6 +136,7 @@ ): Unit = { painter_rendering = null painter_clip = null + painter_gfx_range = null caret_focus = Rendering.Focus.empty } } @@ -356,7 +359,7 @@ for { Text.Info(range, c) <- rendering.background(Rendering.background_elements, line_range, caret_focus) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(rendering.color(c)) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) @@ -366,7 +369,7 @@ for { info <- active_area.info Text.Info(range, _) <- info.try_restrict(line_range) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(rendering.active_hover_color) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) @@ -375,7 +378,7 @@ // squiggly underline for { Text.Info(range, c) <- rendering.squiggly_underline(line_range) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(rendering.color(c)) val x0 = (r.x / 2) * 2 @@ -392,7 +395,7 @@ spell <- rendering.spell_checker(line_range) text <- JEdit_Lib.get_text(buffer, spell.range) info <- spell_checker.marked_words(spell.range.start, text) - r <- JEdit_Lib.gfx_range(text_area, info.range) + r <- painter_gfx_range(info.range) } { gfx.setColor(rendering.spell_checker_color) val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2)) @@ -581,7 +584,7 @@ // bullet bar for { Text.Info(range, color) <- rendering.bullet(line_range) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(color) gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y, @@ -617,7 +620,7 @@ // foreground color for { Text.Info(range, c) <- rendering.foreground(line_range) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(rendering.color(c)) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) @@ -627,7 +630,7 @@ for { regex <- search_pattern range <- JEdit_Lib.search_text(buffer, line_range, regex) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(rendering.search_color) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) @@ -637,7 +640,7 @@ for { info <- highlight_area.info Text.Info(range, color) <- info.try_restrict(line_range) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(color) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) @@ -647,7 +650,7 @@ for { info <- hyperlink_area.info Text.Info(range, _) <- info.try_restrict(line_range) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(rendering.hyperlink_color) gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) @@ -657,7 +660,7 @@ if (!active_exists() && caret_visible) { for { Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(color) gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) @@ -669,7 +672,7 @@ for { completion <- Completion_Popup.Text_Area(text_area) Text.Info(range, color) <- completion.rendering(rendering, line_range) - r <- JEdit_Lib.gfx_range(text_area, range) + r <- painter_gfx_range(range) } { gfx.setColor(color) gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)