# HG changeset patch
# User wenzelm
# Date 1621977166 -7200
# Node ID e4d50a660140a7436f457e3e6a2fc506393813f6
# Parent  4606a9cadd83fe5af3804ef9e93af09824593446
tuned;

diff -r 4606a9cadd83 -r e4d50a660140 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Tue May 25 23:04:29 2021 +0200
+++ b/src/Pure/Thy/latex.scala	Tue May 25 23:12:46 2021 +0200
@@ -30,7 +30,7 @@
     var line = 1
     var result = List.empty[String]
 
-    def output(body: XML.Body): Unit =
+    def traverse(body: XML.Body): Unit =
     {
       body.foreach {
         case XML.Wrapped_Elem(_, _, _) =>
@@ -40,14 +40,14 @@
               val s = position(Value.Int(line), Value.Int(l))
               if (positions.head != s) positions ::= s
             }
-            output(body)
+            traverse(body)
           }
         case XML.Text(s) =>
           line += s.count(_ == '\n')
           result ::= s
       }
     }
-    output(latex_text)
+    traverse(latex_text)
 
     result.reverse.mkString + cat_lines(positions.reverse)
   }