src/Pure/Thy/latex.scala

--- a/src/Pure/Thy/latex.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -67,8 +67,8 @@
         case None => None
         case Some(file) =>
           val source_line =
-            (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))(
-              { case (_, (_, n)) => n })
+            source_lines.iterator.takeWhile({ case (m, _) => m <= l }).
+              foldLeft(0) { case (_, (_, n)) => n }
           if (source_line == 0) None else Some(Position.Line_File(source_line, file))
       }