--- a/src/Pure/Admin/build_log.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Admin/build_log.scala Fri Jun 28 21:01:57 2024 +0200
@@ -650,14 +650,14 @@
): Option[Bytes] =
if (errors.isEmpty) None
else {
- Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
+ Some(YXML.bytes_of_body(XML.Encode.list(XML.Encode.string)(errors)).
compress(cache = cache))
}
def uncompress_errors(bytes: Bytes, cache: XML.Cache = XML.Cache.make()): List[String] =
if (bytes.is_empty) Nil
else {
- XML.Decode.list(YXML.string_of_body)(
+ XML.Decode.list(YXML.string_of_body(_))(
YXML.parse_body(bytes.uncompress(cache = cache.compress).text, cache = cache))
}
--- a/src/Pure/Build/build.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Build/build.scala Fri Jun 28 21:01:57 2024 +0200
@@ -714,13 +714,12 @@
theory_context: Export.Theory_Context,
unicode_symbols: Boolean = false
): Option[Document.Snapshot] = {
- def decode_bytes(bytes: Bytes): String =
- Symbol.output(unicode_symbols, bytes.text)
+ def decode(str: String): String = Symbol.output(unicode_symbols, str)
def read(name: String): Export.Entry = theory_context(name, permissive = true)
def read_xml(name: String): XML.Body =
- YXML.parse_body(decode_bytes(read(name).bytes), cache = theory_context.cache)
+ YXML.parse_body(read(name).bytes.text, recode = decode, cache = theory_context.cache)
def read_source_file(name: String): Store.Source_File =
theory_context.session_context.source_file(name)
@@ -741,14 +740,14 @@
val file = read_source_file(name)
val bytes = file.bytes
- val text = decode_bytes(bytes)
+ val text = decode(bytes.text)
val chunk = Symbol.Text_Chunk(text)
Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) ->
Document.Blobs.Item(bytes, text, chunk, changed = false)
}
- val thy_source = decode_bytes(read_source_file(thy_file).bytes)
+ val thy_source = decode(read_source_file(thy_file).bytes.text)
val thy_xml = read_xml(Export.MARKUP)
val blobs_xml =
for (i <- (1 to blobs.length).toList)
--- a/src/Pure/Build/build_job.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Build/build_job.scala Fri Jun 28 21:01:57 2024 +0200
@@ -294,7 +294,7 @@
val args =
Protocol.Export.Args(
theory_name = theory_name, name = name, compress = compress)
- val body = Bytes(Symbol.encode(YXML.string_of_body(xml)))
+ val body = YXML.bytes_of_body(xml, recode = Symbol.encode)
export_consumer.make_entry(session_name, args, body)
}
}
--- a/src/Pure/Build/export.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Build/export.scala Fri Jun 28 21:01:57 2024 +0200
@@ -194,7 +194,8 @@
def text: String = bytes.text
- def yxml: XML.Body = YXML.parse_body(bytes.text, cache = cache)
+ def yxml(recode: String => String = identity): XML.Body =
+ YXML.parse_body(bytes.text, recode = recode, cache = cache)
}
def make_regex(pattern: String): Regex = {
@@ -536,9 +537,9 @@
def apply(name: String, permissive: Boolean = false): Entry =
session_context.apply(theory, name, permissive = permissive)
- def yxml(name: String): XML.Body =
+ def yxml(name: String, recode: String => String = identity): XML.Body =
get(name) match {
- case Some(entry) => entry.yxml
+ case Some(entry) => entry.yxml(recode = recode)
case None => Nil
}
--- a/src/Pure/Build/export_theory.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Build/export_theory.scala Fri Jun 28 21:01:57 2024 +0200
@@ -391,7 +391,7 @@
for { entry <- theory_context.get(Export.PROOFS_PREFIX + id.serial) }
yield {
- val body = entry.yxml
+ val body = entry.yxml()
val (typargs, (args, (prop_body, proof_body))) = {
import XML.Decode._
import Term_XML.Decode._
--- a/src/Pure/General/bytes.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/bytes.scala Fri Jun 28 21:01:57 2024 +0200
@@ -17,6 +17,7 @@
import com.github.luben.zstd
import scala.collection.mutable.ArrayBuffer
+import scala.collection.mutable
object Bytes {
@@ -168,70 +169,86 @@
}
final class Builder private[Bytes](hint: Long) {
- private var size = 0L
private var chunks =
new ArrayBuffer[Array[Byte]](if (hint <= 0) 16 else (hint / chunk_size).toInt)
+
+ private var buffer_list: mutable.ListBuffer[Array[Byte]] = null
private var buffer =
- new ByteArrayOutputStream(if (hint <= 0) 1024 else (hint min chunk_size min array_size).toInt)
+ new Array[Byte](if (hint <= 0) 1024 else (hint min chunk_size min array_size).toInt)
+ private var buffer_index = 0
+ private var buffer_total = 0
- private def buffer_free(): Int = chunk_size.toInt - buffer.size()
- private def buffer_check(): Unit =
- if (buffer_free() == 0) {
- chunks += buffer.toByteArray
- buffer = new ByteArrayOutputStream(chunk_size.toInt)
+ private def buffer_content(): Array[Byte] =
+ if (buffer_list != null) {
+ val array = new Array[Byte](buffer_total)
+ var i = 0
+ for (b <- buffer_list) {
+ val n = b.length
+ System.arraycopy(b, 0, array, i, n)
+ i += n
+ }
+ System.arraycopy(buffer, 0, array, i, buffer_index)
+ array
+ }
+ else if (buffer_index == buffer.length) buffer else Arrays.copyOf(buffer, buffer_index)
+
+ private def buffer_check(request: Int = 0): Unit =
+ if (buffer_index == buffer.length) {
+ if (buffer_total == chunk_size) {
+ chunks += buffer_content()
+ buffer_list = null
+ buffer = new Array[Byte](chunk_size.toInt)
+ buffer_total = 0
+ buffer_index = 0
+ }
+ else {
+ if (buffer_list == null) { buffer_list = new mutable.ListBuffer }
+ buffer_list += buffer
+ buffer_index = 0
+ val limit = (chunk_size - buffer_total).toInt
+ buffer = new Array[Byte]((buffer_total max request) min limit)
+ }
}
def += (b: Byte): Unit = {
- size += 1
- buffer.write(b)
+ buffer(buffer_index) = b
+ buffer_total += 1
+ buffer_index += 1
buffer_check()
}
- def += (s: CharSequence): Unit = {
- val n = s.length
- if (n > 0) {
- if (UTF8.relevant(s)) { this += UTF8.bytes(s.toString) }
- else {
- var i = 0
- while (i < n) {
- buffer.write(s.charAt(i).toByte)
- size += 1
- i += 1
- buffer_check()
- }
- }
- }
- }
-
def += (array: Array[Byte], offset: Int, length: Int): Unit = {
if (offset < 0 || length < 0 || offset.toLong + length.toLong > array.length) {
throw new IndexOutOfBoundsException
}
- else if (length > 0) {
+ else {
var i = offset
var n = length
while (n > 0) {
- val m = buffer_free()
- if (m > 0) {
- val l = m min n
- buffer.write(array, i, l)
- size += l
- i += l
- n -= l
- }
- buffer_check()
+ val l = n min (buffer.length - buffer_index)
+ System.arraycopy(array, i, buffer, buffer_index, l)
+ buffer_total += l
+ buffer_index += l
+ i += l
+ n -= l
+ buffer_check(request = n)
}
}
}
+ def += (s: CharSequence): Unit =
+ if (s.length > 0) { this += UTF8.bytes(s.toString) }
+
def += (array: Array[Byte]): Unit = { this += (array, 0, array.length) }
def += (a: Subarray): Unit = { this += (a.array, a.offset, a.length) }
private def done(): Bytes = {
val cs = chunks.toArray
- val b = buffer.toByteArray
+ val b = buffer_content()
+ val size = cs.foldLeft(b.length.toLong)({ case (n, a) => n + a.length })
chunks = null
+ buffer_list = null
buffer = null
new Bytes(if (cs.isEmpty) None else Some(cs), b, 0L, size)
}
--- a/src/Pure/General/file.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/file.scala Fri Jun 28 21:01:57 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/html.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/html.scala Fri Jun 28 21:01:57 2024 +0200
@@ -170,8 +170,10 @@
hidden: Boolean,
permissive: Boolean
): Unit = {
+ val xml_output = new XML.Output(s)
+
def output_string(str: String): Unit =
- XML.output_string(s, str, permissive = permissive)
+ xml_output.string(str, permissive = permissive)
def output_hidden(body: => Unit): Unit =
if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
@@ -181,11 +183,11 @@
control_block_begin.get(sym) match {
case Some(op) if control_blocks =>
output_hidden(output_string(sym))
- XML.output_elem(s, Markup(op.name, Nil))
+ xml_output.elem(Markup(op.name, Nil))
case _ =>
control_block_end.get(sym) match {
case Some(op) if control_blocks =>
- XML.output_elem_end(s, op.name)
+ xml_output.end_elem(op.name)
output_hidden(output_string(sym))
case _ =>
if (hidden && Symbol.is_control_encoded(sym)) {
@@ -207,9 +209,9 @@
control.get(ctrl) match {
case Some(op) if Symbol.is_controllable(sym) =>
output_hidden(output_symbol(ctrl))
- XML.output_elem(s, Markup(op.name, Nil))
+ xml_output.elem(Markup(op.name, Nil))
output_symbol(sym)
- XML.output_elem_end(s, op.name)
+ xml_output.end_elem(op.name)
case _ =>
output_symbol(ctrl)
output_symbol(sym)
@@ -222,8 +224,9 @@
def output(text: String): String = {
val control_blocks = check_control_blocks(List(XML.Text(text)))
- Library.make_string(output(_, text,
- control_blocks = control_blocks, hidden = false, permissive = true))
+ Library.string_builder() { builder =>
+ output(builder, text, control_blocks = control_blocks, hidden = false, permissive = true)
+ }
}
@@ -234,18 +237,20 @@
"ul", "ol", "dl", "li", "dt", "dd")
def output(s: StringBuilder, xml: XML.Body, hidden: Boolean, structural: Boolean): Unit = {
+ val xml_output = new XML.Output(s)
+
def output_body(body: XML.Body): Unit = {
val control_blocks = check_control_blocks(body)
body foreach {
case XML.Elem(markup, Nil) =>
- XML.output_elem(s, markup, end = true)
+ xml_output.elem(markup, end = true)
case XML.Elem(Markup(Markup.RAW_HTML, _), body) =>
- XML.traverse_text(body)(()) { case (_, raw) => s.append(raw) }
+ XML.traverse_text(body, (), (_, raw) => s.append(raw))
case XML.Elem(markup, ts) =>
if (structural && structural_elements(markup.name)) s += '\n'
- XML.output_elem(s, markup)
+ xml_output.elem(markup)
output_body(ts)
- XML.output_elem_end(s, markup.name)
+ xml_output.end_elem(markup.name)
if (structural && structural_elements(markup.name)) s += '\n'
case XML.Text(txt) =>
output(s, txt, control_blocks = control_blocks, hidden = hidden, permissive = true)
@@ -255,7 +260,9 @@
}
def output(body: XML.Body, hidden: Boolean, structural: Boolean): String =
- Library.make_string(output(_, body, hidden, structural), capacity = XML.text_length(body) * 2)
+ Library.string_builder(hint = XML.text_length(body) * 2) { builder =>
+ output(builder, body, hidden, structural)
+ }
def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String =
output(List(tree), hidden, structural)
--- a/src/Pure/General/json.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/json.scala Fri Jun 28 21:01:57 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 17:13:25 2024 +0200
+++ b/src/Pure/General/latex.scala Fri Jun 28 21:01:57 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/properties.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/properties.scala Fri Jun 28 21:01:57 2024 +0200
@@ -45,7 +45,7 @@
def encode(ps: T): Bytes = {
if (ps.isEmpty) Bytes.empty
- else Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
+ else YXML.bytes_of_body(XML.Encode.properties(ps))
}
def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T = {
@@ -59,7 +59,7 @@
): Bytes = {
if (ps.isEmpty) Bytes.empty
else {
- Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).
+ YXML.bytes_of_body(XML.Encode.list(XML.Encode.properties)(ps)).
compress(options = options, cache = cache)
}
}
--- a/src/Pure/General/scan.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/scan.scala Fri Jun 28 21:01:57 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 17:13:25 2024 +0200
+++ b/src/Pure/General/sql.scala Fri Jun 28 21:01:57 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 17:13:25 2024 +0200
+++ b/src/Pure/General/ssh.scala Fri Jun 28 21:01:57 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 17:13:25 2024 +0200
+++ b/src/Pure/General/symbol.scala Fri Jun 28 21:01:57 2024 +0200
@@ -265,20 +265,33 @@
tab
}
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
+ val n = text.length
+ val relevant = {
+ var i = 0
+ var found = false
+ while (i < n && !found) {
+ val c = text(i)
+ if (min <= c && c <= max) { found = true }
+ i += 1
}
- else { result.append(c); i += 1 }
+ found
}
- result.toString
+ if (relevant) {
+ val matcher = new Symbol.Matcher(text)
+ Library.string_builder(hint = n) { result =>
+ var i = 0
+ while (i < n) {
+ 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 text
}
}
@@ -528,20 +541,20 @@
def encode(text: String): String = symbols.encode(text)
def decode_yxml(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
- YXML.parse_body(decode(text), cache = cache)
+ YXML.parse_body(text, recode = decode, cache = cache)
def decode_yxml_failsafe(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
- YXML.parse_body_failsafe(decode(text), cache = cache)
+ YXML.parse_body_failsafe(text, recode = decode, cache = cache)
- def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body))
+ def encode_yxml(body: XML.Body): String =
+ YXML.string_of_body(body, recode = encode)
def decode_strict(text: String): String = {
val decoded = decode(text)
if (encode(decoded) == text) decoded
else {
val bad = new mutable.ListBuffer[Symbol]
- for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s))
- bad += s
+ for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s)) bad += s
error("Bad Unicode symbols in text: " + commas_quote(bad))
}
}
--- a/src/Pure/General/toml.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/toml.scala Fri Jun 28 21:01:57 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/General/utf8.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/utf8.scala Fri Jun 28 21:01:57 2024 +0200
@@ -20,12 +20,12 @@
def relevant(s: CharSequence): Boolean = {
var i = 0
val n = s.length
- var utf8 = false
- while (i < n && !utf8) {
- if (s.charAt(i) >= 128) { utf8 = true }
+ var found = false
+ while (i < n && !found) {
+ if (s.charAt(i) >= 128) { found = true }
i += 1
}
- utf8
+ found
}
@@ -41,8 +41,7 @@
var rest = 0
def flush(): Unit = {
if (code != -1) {
- if (rest == 0 && Character.isValidCodePoint(code))
- buf.appendCodePoint(code)
+ if (rest == 0 && Character.isValidCodePoint(code)) buf.appendCodePoint(code)
else buf.append('\uFFFD')
code = -1
rest = 0
--- a/src/Pure/Isar/outer_syntax.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Fri Jun 28 21:01:57 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 17:13:25 2024 +0200
+++ b/src/Pure/PIDE/xml.scala Fri Jun 28 21:01:57 2024 +0200
@@ -6,6 +6,8 @@
package isabelle
+import scala.annotation.tailrec
+
object XML {
/** XML trees **/
@@ -15,9 +17,14 @@
type Attribute = Properties.Entry
type Attributes = Properties.T
- sealed abstract class Tree { override def toString: String = string_of_tree(this) }
+ trait Trav
+ case class End(name: String) extends Trav
+
+ sealed abstract class Tree extends Trav {
+ override def toString: String = string_of_tree(this)
+ }
type Body = List[Tree]
- case class Elem(markup: Markup, body: Body) extends Tree {
+ case class Elem(markup: Markup, body: Body) extends Tree with Trav {
private lazy val hash: Int = (markup, body).hashCode()
override def hashCode(): Int = hash
@@ -29,11 +36,31 @@
def + (att: Attribute): Elem = Elem(markup + att, body)
}
- case class Text(content: String) extends Tree {
+ case class Text(content: String) extends Tree with Trav {
private lazy val hash: Int = content.hashCode()
override def hashCode(): Int = hash
}
+ trait Traversal {
+ def text(s: String): Unit
+ def elem(markup: Markup, end: Boolean = false): Unit
+ def end_elem(name: String): Unit
+
+ def traverse(trees: List[Tree]): Unit = {
+ @tailrec def trav(list: List[Trav]): Unit =
+ (list : @unchecked) match {
+ case Nil =>
+ case Text(s) :: rest => text(s); trav(rest)
+ case Elem(markup, body) :: rest =>
+ if (markup.is_empty) trav(body ::: rest)
+ else if (body.isEmpty) { elem(markup, end = true); trav(rest) }
+ else { elem(markup); trav(body ::: End(markup.name) :: rest) }
+ case End(name) :: rest => end_elem(name); trav(rest)
+ }
+ trav(trees)
+ }
+ }
+
def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
@@ -95,27 +122,24 @@
/* traverse text */
- def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = {
- def traverse(x: A, t: Tree): A =
- t match {
- case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse)
- case XML.Elem(_, ts) => ts.foldLeft(x)(traverse)
- case XML.Text(s) => op(x, s)
+ def traverse_text[A](body: Body, a: A, op: (A, String) => A): A = {
+ @tailrec def trav(x: A, list: List[Tree]): A =
+ list match {
+ case Nil => x
+ case XML.Wrapped_Elem(_, _, body) :: rest => trav(x, body ::: rest)
+ case XML.Elem(_, body) :: rest => trav(x, body ::: rest)
+ case XML.Text(s) :: rest => trav(op(x, s), rest)
}
- body.foldLeft(a)(traverse)
+ trav(a, body)
}
- def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
- def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) }
-
-
- /* text content */
+ 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)(()) { case (_, 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))
@@ -125,66 +149,58 @@
val header: String = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
- def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit = {
- c match {
- case '<' => s ++= "<"
- case '>' => s ++= ">"
- case '&' => s ++= "&"
- case '"' if !permissive => s ++= """
- case '\'' if !permissive => s ++= "'"
- case _ => s += c
+ class Output(builder: StringBuilder) extends Traversal {
+ def string(str: String, permissive: Boolean = false): Unit = {
+ if (str == null) { builder ++= str }
+ else {
+ str foreach {
+ case '<' => builder ++= "<"
+ case '>' => builder ++= ">"
+ case '&' => builder ++= "&"
+ case '"' if !permissive => builder ++= """
+ case '\'' if !permissive => builder ++= "'"
+ case c => builder += c
+ }
+ }
}
- }
+
+ override def text(str: String): Unit = string(str)
- def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit = {
- if (str == null) s ++= str
- else str.iterator.foreach(output_char(s, _, permissive = permissive))
+ override def elem(markup: Markup, end: Boolean = false): Unit = {
+ builder += '<'
+ builder ++= markup.name
+ for ((a, b) <- markup.properties) {
+ builder += ' '
+ builder ++= a
+ builder += '='
+ builder += '"'
+ string(b)
+ builder += '"'
+ }
+ if (end) builder += '/'
+ builder += '>'
+ }
+
+ def end_elem(name: String): Unit = {
+ builder += '<'
+ builder += '/'
+ builder ++= name
+ builder += '>'
+ }
+
+ def result(ts: List[Tree]): String = { traverse(ts); builder.toString }
}
- def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit = {
- s += '<'
- s ++= markup.name
- for ((a, b) <- markup.properties) {
- s += ' '
- s ++= a
- s += '='
- s += '"'
- output_string(s, b)
- s += '"'
- }
- if (end) s += '/'
- s += '>'
- }
-
- def output_elem_end(s: StringBuilder, name: String): Unit = {
- s += '<'
- s += '/'
- s ++= name
- s += '>'
- }
-
- def string_of_body(body: Body): String = {
- val s = new StringBuilder
-
- def tree(t: Tree): Unit =
- t match {
- case XML.Elem(markup, Nil) =>
- output_elem(s, markup, end = true)
- case XML.Elem(markup, ts) =>
- output_elem(s, markup)
- ts.foreach(tree)
- output_elem_end(s, markup.name)
- case XML.Text(txt) => output_string(s, txt)
- }
- body.foreach(tree)
- s.toString
- }
+ def string_of_body(body: Body): String =
+ if (body.isEmpty) ""
+ else new Output(new StringBuilder).result(body)
def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
def text(s: String): String = string_of_tree(XML.Text(s))
+
/** cache **/
object Cache {
--- a/src/Pure/PIDE/yxml.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/PIDE/yxml.scala Fri Jun 28 21:01:57 2024 +0200
@@ -14,8 +14,11 @@
object YXML {
/* chunk markers */
- val X = '\u0005'
- val Y = '\u0006'
+ val X_byte: Byte = 5
+ val Y_byte: Byte = 6
+
+ val X = X_byte.toChar
+ val Y = Y_byte.toChar
val is_X: Char => Boolean = _ == X
val is_Y: Char => Boolean = _ == Y
@@ -31,31 +34,54 @@
/* string representation */
- def traversal(string: String => Unit, body: XML.Body): Unit = {
- def tree(t: XML.Tree): Unit =
- t match {
- case XML.Elem(markup @ Markup(name, atts), ts) =>
- if (markup.is_empty) ts.foreach(tree)
- else {
- string(XY_string)
- string(name)
- for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
- string(X_string)
- ts.foreach(tree)
- string(XYX_string)
- }
- case XML.Text(text) => string(text)
+ trait Output extends XML.Traversal {
+ def byte(b: Byte): Unit
+ def string(s: String): Unit
+
+ // XML.Traversal
+ override def text(s: String): Unit = string(s)
+ override def elem(markup: Markup, end: Boolean = false): Unit = {
+ byte(X_byte)
+ byte(Y_byte)
+ string(markup.name)
+ for ((a, b) <- markup.properties) {
+ byte(Y_byte)
+ string(a)
+ byte('='.toByte)
+ string(b)
}
- body.foreach(tree)
+ byte(X_byte)
+ if (end) end_elem(markup.name)
+ }
+ override def end_elem(name: String): Unit = {
+ byte(X_byte)
+ byte(Y_byte)
+ byte(X_byte)
+ }
}
- def string_of_body(body: XML.Body): String = {
- val s = new StringBuilder
- traversal(str => s ++= str, body)
- s.toString
+ class Output_String(builder: StringBuilder, recode: String => String = identity) extends Output {
+ override def byte(b: Byte): Unit = { builder += b.toChar }
+ override def string(s: String): Unit = { builder ++= recode(s) }
+ def result(ts: List[XML.Tree]): String = { traverse(ts); builder.toString }
+ }
+
+ class Output_Bytes(builder: Bytes.Builder, recode: String => String = identity) extends Output {
+ override def byte(b: Byte): Unit = { builder += b }
+ override def string(s: String): Unit = { builder += recode(s) }
}
- def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
+ def string_of_body(body: XML.Body, recode: String => String = identity): String =
+ new Output_String(new StringBuilder, recode = recode).result(body)
+
+ def string_of_tree(tree: XML.Tree, recode: String => String = identity): String =
+ string_of_body(List(tree), recode = recode)
+
+ def bytes_of_body(body: XML.Body, recode: String => String = identity): Bytes =
+ Bytes.Builder.use()(builder => new Output_Bytes(builder, recode = recode).traverse(body))
+
+ def bytes_of_tree(tree: XML.Tree, recode: String => String = identity): Bytes =
+ bytes_of_body(List(tree), recode = recode)
/* parsing */
@@ -67,11 +93,19 @@
if (name == "") err("unbalanced element")
else err("unbalanced element " + quote(name))
- private def parse_attrib(source: CharSequence): (String, String) =
- Properties.Eq.unapply(source.toString) getOrElse err_attribute()
+ def parse_body(
+ source: CharSequence,
+ recode: String => String = identity,
+ cache: XML.Cache = XML.Cache.none
+ ): XML.Body = {
+ /* parse + recode */
+
+ def parse_string(s: CharSequence): String = recode(s.toString)
+
+ def parse_attrib(s: CharSequence): (String, String) =
+ Properties.Eq.unapply(parse_string(s)) getOrElse err_attribute()
- def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = {
/* stack operations */
def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
@@ -100,8 +134,9 @@
else {
Library.separated_chunks(is_Y, chunk).toList match {
case ch :: name :: atts if ch.length == 0 =>
- push(name.toString, atts.map(parse_attrib))
- case txts => for (txt <- txts) add(cache.tree0(XML.Text(cache.string(txt.toString))))
+ push(parse_string(name), atts.map(parse_attrib))
+ case txts =>
+ for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt)))))
}
}
}
@@ -111,15 +146,23 @@
}
}
- def parse(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
- parse_body(source, cache = cache) match {
+ def parse(
+ source: CharSequence,
+ recode: String => String = identity,
+ cache: XML.Cache = XML.Cache.none
+ ): XML.Tree =
+ parse_body(source, recode = recode, cache = cache) match {
case List(result) => result
case Nil => XML.no_text
case _ => err("multiple XML trees")
}
- def parse_elem(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
- parse_body(source, cache = cache) match {
+ def parse_elem(
+ source: CharSequence,
+ recode: String => String = identity,
+ cache: XML.Cache = XML.Cache.none
+ ): XML.Tree =
+ parse_body(source, recode = recode, cache = cache) match {
case List(elem: XML.Elem) => elem
case _ => err("single XML element expected")
}
@@ -130,13 +173,21 @@
private def markup_broken(source: CharSequence) =
XML.Elem(Markup.Broken, List(XML.Text(source.toString)))
- def parse_body_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = {
- try { parse_body(source, cache = cache) }
+ def parse_body_failsafe(
+ source: CharSequence,
+ recode: String => String = identity,
+ cache: XML.Cache = XML.Cache.none
+ ): XML.Body = {
+ try { parse_body(source, recode = recode, cache = cache) }
catch { case ERROR(_) => List(markup_broken(source)) }
}
- def parse_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree = {
- try { parse(source, cache = cache) }
+ def parse_failsafe(
+ source: CharSequence,
+ recode: String => String = identity,
+ cache: XML.Cache = XML.Cache.none
+ ): XML.Tree = {
+ try { parse(source, recode = recode, cache = cache) }
catch { case ERROR(_) => markup_broken(source) }
}
}
--- a/src/Pure/ROOT.ML Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/ROOT.ML Fri Jun 28 21:01:57 2024 +0200
@@ -372,4 +372,3 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
-
--- a/src/Pure/Tools/dump.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Tools/dump.scala Fri Jun 28 21:01:57 2024 +0200
@@ -33,8 +33,7 @@
write(file_name, Bytes(text))
def write(file_name: Path, body: XML.Body): Unit =
- using(File.writer(write_path(file_name).file))(
- writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body))
+ write(file_name, YXML.bytes_of_body(body, recode = Symbol.encode))
}
sealed case class Aspect(
--- a/src/Pure/library.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/library.scala Fri Jun 28 21:01:57 2024 +0200
@@ -143,10 +143,10 @@
/* strings */
- def make_string(f: StringBuilder => Unit, capacity: Int = 16): String = {
- val s = new StringBuilder(capacity)
- f(s)
- s.toString
+ def string_builder(hint: Int = 0)(body: StringBuilder => Unit): String = {
+ val builder = new StringBuilder(if (hint <= 0) 16 else hint)
+ body(builder)
+ builder.toString
}
def try_unprefix(prfx: String, s: String): Option[String] =
@@ -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/pretty_tooltip.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Jun 28 21:01:57 2024 +0200
@@ -251,7 +251,7 @@
val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
val lines =
- XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
+ XML.traverse_text(formatted, if (XML.text_length(formatted) == 0) 0 else 1,
(n: Int, s: String) => n + Library.count_newlines(s))
val h = painter.getLineHeight * lines + geometry.deco_height
--- a/src/Tools/jEdit/src/syntax_style.scala Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala Fri Jun 28 21:01:57 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)