expose bibtex errors;
authorwenzelm
Thu Dec 14 21:09:41 2017 +0100 (17 months ago)
changeset 6720385784e16bec8
parent 67202 30e863ad5a1a
child 67204 849a838f7e57
expose bibtex errors;
NEWS
src/Pure/Thy/present.scala
src/Pure/Tools/bibtex.scala
     1.1 --- a/NEWS	Thu Dec 14 14:34:56 2017 +0100
     1.2 +++ b/NEWS	Thu Dec 14 21:09:41 2017 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4  
     1.5  * Command-line tool "isabelle document" has been re-implemented in
     1.6  Isabelle/Scala, with simplified arguments and explicit errors from the
     1.7 -latex process. Minor INCOMPATIBILITY.
     1.8 +latex and bibtex process. Minor INCOMPATIBILITY.
     1.9  
    1.10  
    1.11  *** HOL ***
     2.1 --- a/src/Pure/Thy/present.scala	Thu Dec 14 14:34:56 2017 +0100
     2.2 +++ b/src/Pure/Thy/present.scala	Thu Dec 14 21:09:41 2017 +0100
     2.3 @@ -208,7 +208,8 @@
     2.4      /* result */
     2.5  
     2.6      if (!result.ok) {
     2.7 -      cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
     2.8 +      cat_error(
     2.9 +        cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)),
    2.10          "Failed to build document in " + File.path(dir.absolute_file))
    2.11      }
    2.12  
     3.1 --- a/src/Pure/Tools/bibtex.scala	Thu Dec 14 14:34:56 2017 +0100
     3.2 +++ b/src/Pure/Tools/bibtex.scala	Thu Dec 14 21:09:41 2017 +0100
     3.3 @@ -14,6 +14,30 @@
     3.4  
     3.5  object Bibtex
     3.6  {
     3.7 +  /** bibtex errors **/
     3.8 +
     3.9 +  def bibtex_errors(dir: Path, root_name: String): List[String] =
    3.10 +  {
    3.11 +    val log_path = dir + Path.explode(root_name).ext("blg")
    3.12 +    if (log_path.is_file) {
    3.13 +      val Error = """^(.*)---line (\d+) of file (.+)""".r
    3.14 +      Line.logical_lines(File.read(log_path)).flatMap(line =>
    3.15 +        line match {
    3.16 +          case Error(msg, Value.Int(l), file) =>
    3.17 +            val path = File.standard_path(file)
    3.18 +            if (Path.is_wellformed(path)) {
    3.19 +              val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode)
    3.20 +              Some("Bibtex error" + Position.here(pos) + ":\n  " + msg)
    3.21 +            }
    3.22 +            else None
    3.23 +          case _ => None
    3.24 +        })
    3.25 +    }
    3.26 +    else Nil
    3.27 +  }
    3.28 +
    3.29 +
    3.30 +
    3.31    /** document model **/
    3.32  
    3.33    def check_name(name: String): Boolean = name.endsWith(".bib")