# HG changeset patch
# User wenzelm
# Date 1542139074 -3600
# Node ID 085f31ae902d8b52f80efdc0db8d70c8feed21df
# Parent  72a9860f86020c6396db3e15ca6fc34d61be5bef
more robust;

diff -r 72a9860f8602 -r 085f31ae902d src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Tue Nov 13 12:37:46 2018 +0100
+++ b/src/Pure/Thy/bibtex.scala	Tue Nov 13 20:57:54 2018 +0100
@@ -125,19 +125,22 @@
       val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil
 
       val (errors, warnings) =
-        lines.zip(lines.tail ::: List("")).flatMap(
-          {
-            case (Error(msg, Value.Int(l)), _) =>
-              Some((true, (msg, get_line_pos(l))))
-            case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
-              Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name))))
-            case (Warning(msg), Warning_Line(Value.Int(l))) =>
-              Some((false, (Word.capitalize(msg), get_line_pos(l))))
-            case (Warning(msg), _) =>
-              Some((false, (Word.capitalize(msg), Position.none)))
-            case _ => None
-          }
-        ).partition(_._1)
+        if (lines.isEmpty) (Nil, Nil)
+        else {
+          lines.zip(lines.tail ::: List("")).flatMap(
+            {
+              case (Error(msg, Value.Int(l)), _) =>
+                Some((true, (msg, get_line_pos(l))))
+              case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
+                Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name))))
+              case (Warning(msg), Warning_Line(Value.Int(l))) =>
+                Some((false, (Word.capitalize(msg), get_line_pos(l))))
+              case (Warning(msg), _) =>
+                Some((false, (Word.capitalize(msg), Position.none)))
+              case _ => None
+            }
+          ).partition(_._1)
+        }
       (errors.map(_._2), warnings.map(_._2))
     })
   }