--- 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)))
--- 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 {
--- 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
}
--- 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
--- 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("\"", "\"\""))))
--- 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
}
--- 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
}
}
--- 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)
+ }
}
}
--- 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(
--- 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))
--- 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 {
--- 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)