tuned -- avoid odd compiler warning;

--- a/src/Pure/Thy/latex.scala	Wed Apr 22 18:16:48 2020 +0200
+++ b/src/Pure/Thy/latex.scala	Wed Apr 22 18:37:09 2020 +0200
@@ -147,7 +147,8 @@
 
     def error_suffix1(lines: List[String]): Option[String] =
     {
-      val lines1 = lines.take(20).takeWhile({ case File_Line_Error(_) => false case _ => true })
+      val lines1 =
+        lines.take(20).takeWhile({ case File_Line_Error((_, _, _)) => false case _ => true })
       lines1.zipWithIndex.collectFirst({
         case (Line_Error(msg), i) =>
           cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })