# HG changeset patch
# User wenzelm
# Date 1636569930 -3600
# Node ID 95643a0bff4950dcc36f8ba2bdc2189cbd6bf91a
# Parent  10991d115fff768eb979fdc0f4d52f0a72acf4eb
tuned;

diff -r 10991d115fff -r 95643a0bff49 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Wed Nov 10 14:10:42 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Wed Nov 10 19:45:30 2021 +0100
@@ -10,6 +10,7 @@
 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
+import scala.collection.mutable
 import scala.util.matching.Regex
 
 
@@ -21,14 +22,16 @@
 
   def output(latex_text: Text, file_pos: String = ""): String =
   {
-    def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%"
+    var line = 1
+    val result = new mutable.ListBuffer[String]
+    val positions = new mutable.ListBuffer[String]
 
-    var positions: List[String] =
-      if (file_pos.isEmpty) Nil
-      else List(position(Markup.FILE, file_pos), "\\endinput")
+    def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%\n"
 
-    var line = 1
-    var result = List.empty[String]
+    if (file_pos.nonEmpty) {
+      positions += "\\endinput\n"
+      positions += position(Markup.FILE, file_pos)
+    }
 
     def traverse(body: XML.Body): Unit =
     {
@@ -38,18 +41,19 @@
           if (markup.name == Markup.DOCUMENT_LATEX) {
             for { l <- Position.Line.unapply(markup.properties) if positions.nonEmpty } {
               val s = position(Value.Int(line), Value.Int(l))
-              if (positions.head != s) positions ::= s
+              if (positions.last != s) positions += s
             }
             traverse(body)
           }
         case XML.Text(s) =>
           line += s.count(_ == '\n')
-          result ::= s
+          result += s
       }
     }
     traverse(latex_text)
 
-    result.reverse.mkString + cat_lines(positions.reverse)
+    result ++= positions
+    result.mkString
   }