--- 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 ++= "<html><b>"
s ++= line.toString
s ++= ":</b> "
@@ -65,7 +64,6 @@
}
if (last < line_text.length) s ++= line_text.substring(last)
s ++= "</html>"
- s.toString
}
override def toString: String = gui_text
}