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