# HG changeset patch # User wenzelm # Date 1751106123 -7200 # Node ID ddb68e3058d3d5bf072b372fe9e9bd0d4b1105ff # Parent 29d8d6d8a3b14b233c88defa3e0238674a91c301 tuned; diff -r 29d8d6d8a3b1 -r ddb68e3058d3 src/Pure/General/latex.scala --- a/src/Pure/General/latex.scala Sat Jun 28 12:17:48 2025 +0200 +++ b/src/Pure/General/latex.scala Sat Jun 28 12:22:03 2025 +0200 @@ -254,7 +254,7 @@ ): String = { var line = 1 val result = new mutable.ListBuffer[String] - val positions = new mutable.ListBuffer[String] ++= init_position(file_pos) + val positions = mutable.ListBuffer.from(init_position(file_pos)) val file_position = if (file_pos.isEmpty) Position.none else Position.File(file_pos) diff -r 29d8d6d8a3b1 -r ddb68e3058d3 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sat Jun 28 12:17:48 2025 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Sat Jun 28 12:22:03 2025 +0200 @@ -326,7 +326,7 @@ val reparse_set = reparse.toSet var nodes = nodes0 - val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 + val doc_edits = mutable.ListBuffer.from(doc_edits0) val node_edits = (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)