# HG changeset patch
# User wenzelm
# Date 1513183337 -3600
# Node ID eb29f4868d1476b81455fe6e8d168cf872b5a768
# Parent  6be90977f882bed12f9e0ed4cb50afc78cec4e56
more error information according to @<Print type of token list@> in pdfweb.tex;

diff -r 6be90977f882 -r eb29f4868d14 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Wed Dec 13 16:42:02 2017 +0100
+++ b/src/Pure/Thy/latex.scala	Wed Dec 13 17:42:17 2017 +0100
@@ -116,15 +116,25 @@
         }
     }
 
-    object Line_Error
-    {
-      val Pattern = """^l\.(\d+) (.*)$""".r
-      def unapply(line: String): Option[(Int, String)] =
-        line match {
-          case Pattern(Value.Int(line), message) => Some((line, message))
-          case _ => None
-        }
-    }
+    val More_Error =
+      List(
+        """l\.\d+""",
+        "<argument>",
+        "<template>",
+        "<recently read>",
+        "<to be read again>",
+        "<inserted text>",
+        "<output>",
+        "<everypar>",
+        "<everymath>",
+        "<everydisplay>",
+        "<everyhbox>",
+        "<everyvbox>",
+        "<everyjob>",
+        "<everycr>",
+        "<mark>",
+        "<everyeof>",
+        "<write>").mkString("^(?:", "|", ") (.*)$").r
 
     @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
       : List[(String, Position.T)] =
@@ -133,7 +143,7 @@
         case File_Line_Error((file, line, msg1)) :: rest1 =>
           val pos = tex_file_position(file, line)
           rest1 match {
-            case Line_Error((line2, msg2)) :: rest2 if line == line2 =>
+            case More_Error(msg2) :: rest2 =>
               filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
             case _ =>
               filter(rest1, (msg1, pos) :: result)