# HG changeset patch
# User wenzelm
# Date 1616502435 -3600
# Node ID 4e12a6caefb3a0580fc3bf99591bda89fd3d1d3f
# Parent  2cc9bd9a735741f123fca1433a0fa83102a4dc8d
turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont;

diff -r 2cc9bd9a7357 -r 4e12a6caefb3 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Tue Mar 23 13:13:31 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Tue Mar 23 13:27:15 2021 +0100
@@ -138,6 +138,7 @@
         "<everyeof>",
         "<write>").mkString("^(?:", "|", ") (.*)$").r
 
+    val Bad_Font = """^LaTeX Font Warning: (Font .*\btxmia\b.* undefined).*$""".r
     val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r
 
     val error_ignore =
@@ -167,6 +168,8 @@
           val pos = tex_file_position(file, line)
           val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
           filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
+        case Bad_Font(msg) :: rest =>
+          filter(rest, (msg, Position.none) :: result)
         case Bad_File(msg) :: rest =>
           filter(rest, (msg, Position.none) :: result)
         case _ :: rest => filter(rest, result)
diff -r 2cc9bd9a7357 -r 4e12a6caefb3 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Tue Mar 23 13:13:31 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Tue Mar 23 13:27:15 2021 +0100
@@ -680,12 +680,15 @@
 
             val log_lines = result.out_lines ::: result.err_lines
 
-            if (!result.ok) {
+            val errors =
+              (if (result.ok) Nil else List(result.err)) :::
+              Latex.latex_errors(doc_dir, root) :::
+              Bibtex.bibtex_errors(doc_dir, root)
+
+            if (errors.nonEmpty) {
               val message =
                 Exn.cat_message(
-                  result.err,
-                  cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
-                  "Failed to build document " + quote(doc.name))
+                  (errors ::: List("Failed to build document " + quote(doc.name))):_*)
               throw new Build_Error(log_lines, message)
             }
             else if (!result_path.is_file) {