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