# HG changeset patch
# User wenzelm
# Date 1587573429 -7200
# Node ID 8a5da740e388ff7a6dd68e3dd6d8a65d1308ee36
# Parent  73dee865d567a295b33306f1293af16979c31c51
tuned -- avoid odd compiler warning;

diff -r 73dee865d567 -r 8a5da740e388 src/Pure/Thy/latex.scala
--- 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)) })