# HG changeset patch
# User wenzelm
# Date 1621351159 -7200
# Node ID 2f023b2b0e1ea1532316594ebe43cc81c7cbab13
# Parent  4b1d8beed8a3c5116ba6aaff7bc2e61d1ac5b4b5
more uniform bibtex error, without using perl (see 4710dd5093a3);

diff -r 4b1d8beed8a3 -r 2f023b2b0e1e lib/Tools/latex
--- a/lib/Tools/latex	Tue May 18 17:02:45 2021 +0200
+++ b/lib/Tools/latex	Tue May 18 17:19:19 2021 +0200
@@ -80,9 +80,6 @@
     check_root
     $ISABELLE_BIBTEX </dev/null "$FILEBASE"
     RC="$?"
-    if [ "$RC" -gt 0 -a -f "${FILEBASE}.blg" ]; then
-      perl -n -e 'if (m/^I (found no.*$)/) { print "bibtex $1\n"; }' "${FILEBASE}.blg" >&2
-    fi
     ;;
   idx)
     check_root
diff -r 4b1d8beed8a3 -r 2f023b2b0e1e src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Tue May 18 17:02:45 2021 +0200
+++ b/src/Pure/Thy/bibtex.scala	Tue May 18 17:19:19 2021 +0200
@@ -55,11 +55,13 @@
     val log_path = dir + Path.explode(root_name).ext("blg")
     if (log_path.is_file) {
       val Error1 = """^(I couldn't open database file .+)$""".r
-      val Error2 = """^(.+)---line (\d+) of file (.+)""".r
+      val Error2 = """^(I found no .+)$""".r
+      val Error3 = """^(.+)---line (\d+) of file (.+)""".r
       Line.logical_lines(File.read(log_path)).flatMap(line =>
         line match {
           case Error1(msg) => Some("Bibtex error: " + msg)
-          case Error2(msg, Value.Int(l), file) =>
+          case Error2(msg) => Some("Bibtex error: " + msg)
+          case Error3(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)