# HG changeset patch
# User wenzelm
# Date 1514572526 -3600
# Node ID 0bfbf5b9d6ba0deda94310d733070777b1bcab6a
# Parent  ba52a058942f89e7182db243bdc89d08e639367a
more accurate message patterns;

diff -r ba52a058942f -r 0bfbf5b9d6ba src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Dec 29 19:17:52 2017 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Dec 29 19:35:26 2017 +0100
@@ -22,10 +22,12 @@
   {
     val log_path = dir + Path.explode(root_name).ext("blg")
     if (log_path.is_file) {
-      val Error = """^(.*)---line (\d+) of file (.+)""".r
+      val Error1 = """^(I couldn't open database file .+)$""".r
+      val Error2 = """^(.+)---line (\d+) of file (.+)""".r
       Line.logical_lines(File.read(log_path)).flatMap(line =>
         line match {
-          case Error(msg, Value.Int(l), file) =>
+          case Error1(msg) => Some("Bibtex error: " + msg)
+          case Error2(msg, Value.Int(l), file) =>
             val path = File.standard_path(file)
             if (Path.is_wellformed(path)) {
               val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode)