Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sat, 28 Jun 2025 12:22:03 +0200
changeset 82787 ddb68e3058d3
parent 82786 29d8d6d8a3b1
child 82788 5afb8d0d418e
tuned;
src/Pure/General/latex.scala file | annotate | diff | comparison | revisions
src/Pure/Thy/thy_syntax.scala file | annotate | diff | comparison | revisions 
--- 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)
 
--- 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)
isabelle