# HG changeset patch # User wenzelm # Date 1719567433 -7200 # Node ID c420429fdf4c843cb327792ff1fba9e926f64eb6 # Parent dfadcfdf8dadbde802d99485c353757ce23d0f6f tuned; diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/General/file.scala --- a/src/Pure/General/file.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/General/file.scala Fri Jun 28 11:37:13 2024 +0200 @@ -205,13 +205,12 @@ def read(path: Path): String = read(path.file) - def read_stream(reader: BufferedReader): String = { - val output = new StringBuilder(100) - var c = -1 - while ({ c = reader.read; c != -1 }) output += c.toChar - reader.close() - output.toString - } + def read_stream(reader: BufferedReader): String = + Library.string_builder(hint = 100) { output => + var c = -1 + while ({ c = reader.read; c != -1 }) output += c.toChar + reader.close() + } def read_stream(stream: InputStream): String = read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/General/json.scala --- a/src/Pure/General/json.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/General/json.scala Fri Jun 28 11:37:13 2024 +0200 @@ -196,49 +196,44 @@ case _ => false } - def apply(json: T): S = { - val result = new StringBuilder - - def output(x: T): Unit = { - if (!output_atom(x, result)) { - x match { - case Object(obj) => - result += '{' - Library.separate(None, obj.toList.map(Some(_))).foreach({ - case None => result += ',' - case Some((x, y)) => - output_string(x, result) - result += ':' - output(y) - }) - result += '}' - case list: List[T] => - result += '[' - Library.separate(None, list.map(Some(_))).foreach({ - case None => result += ',' - case Some(x) => output(x) - }) - result += ']' - case _ => error("Bad JSON value: " + x.toString) + def apply(json: T): S = + Library.string_builder() { result => + def output(x: T): Unit = { + if (!output_atom(x, result)) { + x match { + case Object(obj) => + result += '{' + Library.separate(None, obj.toList.map(Some(_))).foreach({ + case None => result += ',' + case Some((x, y)) => + output_string(x, result) + result += ':' + output(y) + }) + result += '}' + case list: List[T] => + result += '[' + Library.separate(None, list.map(Some(_))).foreach({ + case None => result += ',' + case Some(x) => output(x) + }) + result += ']' + case _ => error("Bad JSON value: " + x.toString) + } } } + + output(json) } - output(json) - result.toString - } - private def pretty_atom(x: T): Option[XML.Tree] = { val result = new StringBuilder val ok = output_atom(x, result) if (ok) Some(XML.Text(result.toString)) else None } - private def pretty_string(s: String): XML.Tree = { - val result = new StringBuilder - output_string(s, result) - XML.Text(result.toString) - } + private def pretty_string(s: String): XML.Tree = + XML.Text(Library.string_builder()(output_string(s, _))) private def pretty_tree(x: T): XML.Tree = x match { diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/General/latex.scala --- a/src/Pure/General/latex.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/General/latex.scala Fri Jun 28 11:37:13 2024 +0200 @@ -34,14 +34,14 @@ def output_name(name: String): String = if (name.exists(output_name_map.keySet)) { - val res = new StringBuilder - for (c <- name) { - output_name_map.get(c) match { - case None => res += c - case Some(s) => res ++= s + Library.string_builder() { res => + for (c <- name) { + output_name_map.get(c) match { + case None => res += c + case Some(s) => res ++= s + } } } - res.toString } else name @@ -52,18 +52,18 @@ val special1 = "!\"@|" val special2 = "\\{}#" if (str.exists(c => special1.contains(c) || special2.contains(c))) { - val res = new StringBuilder - for (c <- str) { - if (special1.contains(c)) { - res ++= "\\char" - res ++= Value.Int(c) - } - else { - if (special2.contains(c)) { res += '"'} - res += c + Library.string_builder() { res => + for (c <- str) { + if (special1.contains(c)) { + res ++= "\\char" + res ++= Value.Int(c) + } + else { + if (special2.contains(c)) { res += '"'} + res += c + } } } - res.toString } else str } diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/General/scan.scala Fri Jun 28 11:37:13 2024 +0200 @@ -386,11 +386,10 @@ if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j) else throw new IndexOutOfBoundsException - override def toString: String = { - val buf = new StringBuilder(length) - for (offset <- start until end) buf.append(seq(offset)) - buf.toString - } + override def toString: String = + Library.string_builder(hint = length) { buf => + for (offset <- start until end) buf.append(seq(offset)) + } } abstract class Byte_Reader extends Reader[Char] with AutoCloseable diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/General/sql.scala Fri Jun 28 11:37:13 2024 +0200 @@ -29,18 +29,17 @@ /* concrete syntax */ - def string(s: String): Source = { - val q = '\'' - val result = new StringBuilder(s.length + 10) - result += q - for (c <- s.iterator) { - if (c == '\u0000') error("Illegal NUL character in SQL string literal") - if (c == q) result += q - result += c + def string(s: String): Source = + Library.string_builder(hint = s.length + 10) { result => + val q = '\'' + result += q + for (c <- s.iterator) { + if (c == '\u0000') error("Illegal NUL character in SQL string literal") + if (c == q) result += q + result += c + } + result += q } - result += q - result.toString - } def ident(s: String): Source = Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\"")))) diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/General/ssh.scala Fri Jun 28 11:37:13 2024 +0200 @@ -70,12 +70,12 @@ val special = "[]?*\\{} \"'" if (str.isEmpty) "\"\"" else if (str.exists(special.contains)) { - val res = new StringBuilder - for (c <- str) { - if (special.contains(c)) res += '\\' - res += c + Library.string_builder() { res => + for (c <- str) { + if (special.contains(c)) res += '\\' + res += c + } } - res.toString() } else str } diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/General/symbol.scala Fri Jun 28 11:37:13 2024 +0200 @@ -267,18 +267,18 @@ def recode(text: String): String = { val len = text.length val matcher = new Symbol.Matcher(text) - val result = new StringBuilder(len) - var i = 0 - while (i < len) { - val c = text(i) - if (min <= c && c <= max) { - val s = matcher.match_symbol(i) - result.append(table.getOrElse(s, s)) - i += s.length + Library.string_builder(hint = len) { result => + var i = 0 + while (i < len) { + val c = text(i) + if (min <= c && c <= max) { + val s = matcher.match_symbol(i) + result.append(table.getOrElse(s, s)) + i += s.length + } + else { result.append(c); i += 1 } } - else { result.append(c); i += 1 } } - result.toString } } diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/General/toml.scala --- a/src/Pure/General/toml.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/General/toml.scala Fri Jun 28 11:37:13 2024 +0200 @@ -614,94 +614,90 @@ private def keys(ks: List[Key]): Str = ks.map(key).mkString(".") - private def inline(t: T, indent: Int = 0): Str = { - val result = new StringBuilder - - result ++= Symbol.spaces(indent * 2) - (t: @unchecked) match { - case s: String => - if (s.rep.contains("\n") && s.rep.length > 20) result ++= multiline_basic_string(s.rep) - else result ++= basic_string(s.rep) - case a: Array => - if (a.is_empty) result ++= "[]" - else { - result ++= "[\n" - a.any.values.foreach { elem => - result ++= inline(elem, indent + 1) - result ++= ",\n" - } - result ++= Symbol.spaces(indent * 2) - result += ']' - } - case table: Table => - if (table.is_empty) result ++= "{}" - else { - result ++= "{ " - Library.separate(None, table.any.values.map(Some(_))).foreach { - case None => result ++= ", " - case Some((k, v)) => - result ++= key(k) - result ++= " = " - result ++= inline(v) + private def inline(t: T, indent: Int = 0): Str = + Library.string_builder() { result => + result ++= Symbol.spaces(indent * 2) + (t: @unchecked) match { + case s: String => + if (s.rep.contains("\n") && s.rep.length > 20) result ++= multiline_basic_string(s.rep) + else result ++= basic_string(s.rep) + case a: Array => + if (a.is_empty) result ++= "[]" + else { + result ++= "[\n" + a.any.values.foreach { elem => + result ++= inline(elem, indent + 1) + result ++= ",\n" + } + result ++= Symbol.spaces(indent * 2) + result += ']' } - result ++= " }" - } - case Scalar(s) => result ++= s - } - result.toString() - } - - def apply(toml: Table): Str = { - val result = new StringBuilder - - def inline_values(path: List[Key], t: T): Unit = - t match { - case t: Table => t.any.values.foreach { case (k, v1) => inline_values(k :: path, v1) } - case _ => - result ++= keys(path.reverse) - result ++= " = " - result ++= inline(t) - result += '\n' - } - - def is_inline(elem: T): Bool = - elem match { - case _: String | _: Integer | _: Float | _: Boolean | _: Offset_Date_Time | - _: Local_Date_Time | _: Local_Date | _: Local_Time => true - case a: Array => a.any.values.forall(is_inline) - case _ => false - } - def is_table(elem: T): Bool = elem match { case _: Table => true case _ => false } - - def array(path: List[Key], a: Array): Unit = - if (a.any.values.forall(is_inline) || !a.any.values.forall(is_table)) - inline_values(path.take(1), a) - else a.table.values.foreach { t => - result ++= "\n[[" - result ++= keys(path.reverse) - result ++= "]]\n" - table(path, t, is_table_entry = true) - } - - def table(path: List[Key], t: Table, is_table_entry: Bool = false): Unit = { - val (values, nodes) = t.any.values.partition(kv => is_inline(kv._2)) - - if (!is_table_entry && path.nonEmpty) { - result ++= "\n[" - result ++= keys(path.reverse) - result ++= "]\n" - } - - values.foreach { case (k, v) => inline_values(List(k), v) } - nodes.foreach { - case (k, t: Table) => table(k :: path, t) - case (k, arr: Array) => array(k :: path, arr) - case _ => + case table: Table => + if (table.is_empty) result ++= "{}" + else { + result ++= "{ " + Library.separate(None, table.any.values.map(Some(_))).foreach { + case None => result ++= ", " + case Some((k, v)) => + result ++= key(k) + result ++= " = " + result ++= inline(v) + } + result ++= " }" + } + case Scalar(s) => result ++= s } } - table(Nil, toml) - result.toString - } + def apply(toml: Table): Str = + Library.string_builder() { result => + def inline_values(path: List[Key], t: T): Unit = + t match { + case t: Table => t.any.values.foreach { case (k, v1) => inline_values(k :: path, v1) } + case _ => + result ++= keys(path.reverse) + result ++= " = " + result ++= inline(t) + result += '\n' + } + + def is_inline(elem: T): Bool = + elem match { + case _: String | _: Integer | _: Float | _: Boolean | _: Offset_Date_Time | + _: Local_Date_Time | _: Local_Date | _: Local_Time => true + case a: Array => a.any.values.forall(is_inline) + case _ => false + } + def is_table(elem: T): Bool = elem match { case _: Table => true case _ => false } + + def array(path: List[Key], a: Array): Unit = + if (a.any.values.forall(is_inline) || !a.any.values.forall(is_table)) + inline_values(path.take(1), a) + else a.table.values.foreach { t => + result ++= "\n[[" + result ++= keys(path.reverse) + result ++= "]]\n" + table(path, t, is_table_entry = true) + } + + def table(path: List[Key], t: Table, is_table_entry: Bool = false): Unit = { + val (values, nodes) = t.any.values.partition(kv => is_inline(kv._2)) + + if (!is_table_entry && path.nonEmpty) { + result ++= "\n[" + result ++= keys(path.reverse) + result ++= "]\n" + } + + values.foreach { case (k, v) => inline_values(List(k), v) } + nodes.foreach { + case (k, t: Table) => table(k :: path, t) + case (k, arr: Array) => array(k :: path, arr) + case _ => + } + } + + table(Nil, toml) + } } } diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Fri Jun 28 11:37:13 2024 +0200 @@ -20,25 +20,24 @@ /* string literals */ - def quote_string(str: String): String = { - val result = new StringBuilder(str.length + 10) - result += '"' - for (s <- Symbol.iterator(str)) { - if (s.length == 1) { - val c = s(0) - if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') { - result += '\\' - if (c < 10) result += '0' - if (c < 100) result += '0' - result ++= c.asInstanceOf[Int].toString + def quote_string(str: String): String = + Library.string_builder(hint = str.length + 10) { result => + result += '"' + for (s <- Symbol.iterator(str)) { + if (s.length == 1) { + val c = s(0) + if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') { + result += '\\' + if (c < 10) result += '0' + if (c < 100) result += '0' + result ++= c.asInstanceOf[Int].toString + } + else result += c } - else result += c + else result ++= s } - else result ++= s + result += '"' } - result += '"' - result.toString - } } final class Outer_Syntax private( diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/PIDE/xml.scala Fri Jun 28 11:37:13 2024 +0200 @@ -137,11 +137,10 @@ def text_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + s.length) def symbol_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + Symbol.length(s)) - def content(body: Body): String = { - val text = new StringBuilder(text_length(body)) - traverse_text(body, (), (_, s) => text.append(s)) - text.toString - } + def content(body: Body): String = + Library.string_builder(hint = text_length(body)) { text => + traverse_text(body, (), (_, s) => text.append(s)) + } def content(tree: Tree): String = content(List(tree)) diff -r dfadcfdf8dad -r c420429fdf4c src/Pure/library.scala --- a/src/Pure/library.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Pure/library.scala Fri Jun 28 11:37:13 2024 +0200 @@ -194,12 +194,8 @@ if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i) else throw new IndexOutOfBoundsException - override def toString: String = { - val buf = new StringBuilder(length) - for (i <- 0 until length) - buf.append(charAt(i)) - buf.toString - } + override def toString: String = + string_builder(hint = length) { buf => for (i <- 0 until length) buf.append(charAt(i)) } } class Line_Termination(text: CharSequence) extends CharSequence { diff -r dfadcfdf8dad -r c420429fdf4c src/Tools/jEdit/src/syntax_style.scala --- a/src/Tools/jEdit/src/syntax_style.scala Fri Jun 28 11:09:58 2024 +0200 +++ b/src/Tools/jEdit/src/syntax_style.scala Fri Jun 28 11:37:13 2024 +0200 @@ -168,14 +168,13 @@ val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control_sym) - def update_style(text: String): String = { - val result = new StringBuilder - for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) { - if (Symbol.is_controllable(sym)) result ++= control_decoded - result ++= sym + def update_style(text: String): String = + Library.string_builder() { result => + for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) { + if (Symbol.is_controllable(sym)) result ++= control_decoded + result ++= sym + } } - result.toString - } text_area.getSelection.foreach { sel => val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)