# HG changeset patch
# User wenzelm
# Date 1516538428 -3600
# Node ID dce6675376075d8f00e68d80126b885c6ccaf688
# Parent  df252c3d48f2d16aaa75de799db4a12993dc133f
detect more errors;

diff -r df252c3d48f2 -r dce667537607 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Sun Jan 21 11:04:18 2018 +0100
+++ b/src/Pure/Thy/latex.scala	Sun Jan 21 13:40:28 2018 +0100
@@ -137,6 +137,8 @@
         "<everyeof>",
         "<write>").mkString("^(?:", "|", ") (.*)$").r
 
+    val Bad_File = """^! LaTeX Error: File `(.*)' not found\.$""".r
+
     val error_ignore =
       Set(
         "See the LaTeX manual or LaTeX Companion for explanation.",
@@ -163,6 +165,9 @@
           val pos = tex_file_position(file, line)
           val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
           filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
+        case Bad_File(file) :: rest =>
+          val msg = "File " + quote(file) + " not found"
+          filter(rest, (msg, Position.none) :: result)
         case _ :: rest => filter(rest, result)
         case Nil => result.reverse
       }