# HG changeset patch
# User wenzelm
# Date 1607639351 -3600
# Node ID 1dc2ad97e0629b568dc107a10eef3a6b92f58156
# Parent  220a094a42d85bb11b72d4941a3dbdf1a6533f19
more informative error;

diff -r 220a094a42d8 -r 1dc2ad97e062 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Dec 10 22:57:25 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Dec 10 23:29:11 2020 +0100
@@ -448,6 +448,9 @@
   def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
   def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
 
+  class Build_Error(val log_lines: List[String], val message: String)
+    extends Exn.User_Error(message)
+
   def build_documents(
     session: String,
     deps: Sessions.Deps,
@@ -576,14 +579,19 @@
             val root_pdf = Path.basic(root).pdf
             val result_path = doc_dir + root_pdf
 
+            val log_lines = result.out_lines ::: result.err_lines
+
             if (!result.ok) {
-              cat_error(
-                Library.trim_line(result.err),
-                cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
-                "Failed to build document " + quote(doc.name))
+              val message =
+                Exn.cat_message(
+                  Library.trim_line(result.err),
+                  cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
+                  "Failed to build document " + quote(doc.name))
+              throw new Build_Error(log_lines, message)
             }
             else if (!result_path.is_file) {
-              error("Bad document result: expected to find " + root_pdf)
+              val message = "Bad document result: expected to find " + root_pdf
+              throw new Build_Error(log_lines, message)
             }
             else {
               val stop = Time.now()
@@ -591,7 +599,7 @@
               progress.echo("Finished " + session + "/" + doc.name +
                 " (" + timing.message_hms + " elapsed time)")
 
-              val log_xz = Bytes(cat_lines(result.out_lines ::: result.err_lines)).compress()
+              val log_xz = Bytes(cat_lines(log_lines)).compress()
               val pdf = Bytes.read(result_path)
               Document_Output(doc.name, sources, log_xz, pdf)
             }
diff -r 220a094a42d8 -r 1dc2ad97e062 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 22:57:25 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 23:29:11 2020 +0100
@@ -460,7 +460,10 @@
           }
           else (Nil, Nil)
         }
-        catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) }
+        catch {
+          case exn: Presentation.Build_Error => (exn.log_lines, List(exn.message))
+          case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
+        }
 
       val result =
       {