--- 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
}