# HG changeset patch # User wenzelm # Date 1733566382 -3600 # Node ID 2f43a87a7d0628454501a8e3a2496e61f4add7b8 # Parent ee07998f9b259ea98501dd9d3ea62e2b5ce6a999 tuned; diff -r ee07998f9b25 -r 2f43a87a7d06 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Dec 06 23:07:09 2024 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Dec 07 11:13:02 2024 +0100 @@ -43,9 +43,8 @@ lazy val line_text: String = Library.trim_line(JEdit_Lib.get_text(buffer, line_range).getOrElse("")) - lazy val gui_text: String = { + lazy val gui_text: String = Library.string_builder(line_range.length * 2) { s => // see also HyperSearchResults.highlightString - val s = new StringBuilder(line_range.length * 2) s ++= "" s ++= line.toString s ++= ": " @@ -65,7 +64,6 @@ } if (last < line_text.length) s ++= line_text.substring(last) s ++= "" - s.toString } override def toString: String = gui_text }