more accurate error messages;

--- a/src/Pure/Thy/document_build.scala	Wed Dec 21 15:41:45 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Dec 21 22:11:16 2022 +0100
@@ -319,12 +319,12 @@
       val result_pdf = doc_dir + root_pdf
 
       if (errors.nonEmpty) {
-        val errors1 = errors ::: List("Failed to build document " + quote(doc.name))
-        throw new Build_Error(log, Exn.cat_message(errors1: _*))
+        val message = "Failed to build document " + quote(doc.name)
+        throw new Build_Error(log, errors ::: List(message))
       }
       else if (!result_pdf.is_file) {
         val message = "Bad document result: expected to find " + root_pdf
-        throw new Build_Error(log, message)
+        throw new Build_Error(log, List(message))
       }
       else {
         val log_xz = Bytes(cat_lines(log)).compress()
@@ -396,8 +396,15 @@
           watchdog = Time.seconds(0.5))
 
       val log = result.out_lines ::: result.err_lines
-      val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors()
-      directory.make_document(log, errors)
+      val err = result.err
+
+      val errors1 = directory.log_errors()
+      val errors2 =
+        if (result.ok) errors1
+        else if (err.nonEmpty) err :: errors1
+        else if (errors1.nonEmpty) errors1
+        else List("Error")
+      directory.make_document(log, errors2)
     }
   }
 
@@ -429,8 +436,8 @@
 
   def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
 
-  class Build_Error(val log_lines: List[String], val message: String)
-    extends Exn.User_Error(message)
+  class Build_Error(val log_lines: List[String], val log_errors: List[String])
+    extends Exn.User_Error(Exn.cat_message(log_errors: _*))
 
   def build_documents(
     context: Context,

--- a/src/Pure/Tools/build_job.scala	Wed Dec 21 15:41:45 2022 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Dec 21 22:11:16 2022 +0100
@@ -500,7 +500,7 @@
           else (Nil, Nil)
         }
         catch {
-          case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message))
+          case exn: Document_Build.Build_Error => (exn.log_lines, exn.log_errors)
           case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
         }
 

--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Dec 21 15:41:45 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Dec 21 22:11:16 2022 +0100
@@ -214,17 +214,21 @@
       case Some(session_background) if session_background.info.documents.nonEmpty =>
         run_process { progress =>
           show_page(log_page)
-          val res = Exn.capture { document_build(session_background, progress) }
-          val msg =
-            res match {
-              case Exn.Res(_) => Protocol.writeln_message("OK")
-              case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn))
+          val result = Exn.capture { document_build(session_background, progress) }
+          val msgs =
+            result match {
+              case Exn.Res(_) =>
+                List(Protocol.writeln_message("OK"))
+              case Exn.Exn(exn: Document_Build.Build_Error) =>
+                exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(s)))
+              case Exn.Exn(exn) =>
+                List(Protocol.error_message(YXML.parse_body(Exn.print(exn))))
             }
 
-          finish_process(List(msg))
+          finish_process(Pretty.separate(msgs))
 
           show_state()
-          show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
+          show_page(if (Exn.is_interrupt_exn(result)) theories_page else output_page)
         }
       case _ =>
     }