diff -r 09c16e5636ad -r 3e51429404cd src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Fri Dec 27 17:26:51 2024 +0100 +++ b/src/Pure/GUI/gui.scala Fri Dec 27 17:30:59 2024 +0100 @@ -79,13 +79,19 @@ } class Style_HTML extends Style { - override def enclose(body: String): String = "" + body + "" + override def enclose(body: String): String = enclose_style("", body) override def make_text(str: String): String = HTML.output(str) override def make_bold(str: String): String = "" + make_text(str) + "" override def spaces(n: Int): String = HTML.spaces(n) def enclose_style(style: String, body: String): String = - if (style.isEmpty) enclose(body) + if (style.isEmpty) { + Library.string_builder(body.length + 13) { s => + s ++= "" + s ++= body + s ++= "" + } + } else { Library.string_builder(style.length + body.length + 35) { s => s ++= "