expose bibtex errors;

--- a/NEWS	Thu Dec 14 14:34:56 2017 +0100
+++ b/NEWS	Thu Dec 14 21:09:41 2017 +0100
@@ -88,7 +88,7 @@
 
 * Command-line tool "isabelle document" has been re-implemented in
 Isabelle/Scala, with simplified arguments and explicit errors from the
-latex process. Minor INCOMPATIBILITY.
+latex and bibtex process. Minor INCOMPATIBILITY.
 
 
 *** HOL ***

--- a/src/Pure/Thy/present.scala	Thu Dec 14 14:34:56 2017 +0100
+++ b/src/Pure/Thy/present.scala	Thu Dec 14 21:09:41 2017 +0100
@@ -208,7 +208,8 @@
     /* result */
 
     if (!result.ok) {
-      cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
+      cat_error(
+        cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)),
         "Failed to build document in " + File.path(dir.absolute_file))
     }
 

--- a/src/Pure/Tools/bibtex.scala	Thu Dec 14 14:34:56 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala	Thu Dec 14 21:09:41 2017 +0100
@@ -14,6 +14,30 @@
 
 object Bibtex
 {
+  /** bibtex errors **/
+
+  def bibtex_errors(dir: Path, root_name: String): List[String] =
+  {
+    val log_path = dir + Path.explode(root_name).ext("blg")
+    if (log_path.is_file) {
+      val Error = """^(.*)---line (\d+) of file (.+)""".r
+      Line.logical_lines(File.read(log_path)).flatMap(line =>
+        line match {
+          case Error(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)
+              Some("Bibtex error" + Position.here(pos) + ":\n  " + msg)
+            }
+            else None
+          case _ => None
+        })
+    }
+    else Nil
+  }
+
+
+
   /** document model **/
 
   def check_name(name: String): Boolean = name.endsWith(".bib")