# HG changeset patch
# User wenzelm
# Date 1516616622 -3600
# Node ID aae933ca6fbdf958f1ef646757887c51dce808a9
# Parent  dce6675376075d8f00e68d80126b885c6ccaf688
tuned message: same error may occur in different contexts;

diff -r dce667537607 -r aae933ca6fbd src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Sun Jan 21 13:40:28 2018 +0100
+++ b/src/Pure/Thy/latex.scala	Mon Jan 22 11:23:42 2018 +0100
@@ -137,7 +137,7 @@
         "<everyeof>",
         "<write>").mkString("^(?:", "|", ") (.*)$").r
 
-    val Bad_File = """^! LaTeX Error: File `(.*)' not found\.$""".r
+    val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r
 
     val error_ignore =
       Set(
@@ -165,8 +165,7 @@
           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"
+        case Bad_File(msg) :: rest =>
           filter(rest, (msg, Position.none) :: result)
         case _ :: rest => filter(rest, result)
         case Nil => result.reverse