# 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)