# HG changeset patch
# User wenzelm
# Date 1606305120 -3600
# Node ID ed59a506998f6bb76a50eb5667542c9631fa1a1c
# Parent  6f83f7892317ad9ffb08dd14d79304b5165e57a9
clarified document_output vs. progress;

diff -r 6f83f7892317 -r ed59a506998f src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Wed Nov 25 12:34:08 2020 +0100
+++ b/src/Pure/System/progress.scala	Wed Nov 25 12:52:00 2020 +0100
@@ -32,7 +32,6 @@
 
   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
   def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
-  def echo_document(msg: String) { echo(msg) }
 
   def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
     Timing.timeit(message, enabled, echo)(e)
diff -r 6f83f7892317 -r ed59a506998f src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Nov 25 12:34:08 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Wed Nov 25 12:52:00 2020 +0100
@@ -58,6 +58,7 @@
     extends Document_Name
   {
     def log: String = log_xz.uncompress().text
+    def log_lines: List[String] = split_lines(log)
   }
 
 
@@ -508,7 +509,7 @@
       yield {
         Isabelle_System.with_tmp_dir("document")(tmp_dir =>
         {
-          progress.echo_document("Preparing " + session + "/" + doc.name + " ...")
+          progress.echo("Preparing " + session + "/" + doc.name + " ...")
           val start = Time.now()
 
 
@@ -583,7 +584,7 @@
             else {
               val stop = Time.now()
               val timing = stop - start
-              progress.echo_document("Finished " + session + "/" + doc.name +
+              progress.echo("Finished " + session + "/" + doc.name +
                 " (" + timing.message_hms + " elapsed time)")
 
               val log_xz = Bytes(cat_lines(result.out_lines ::: result.err_lines)).compress()
@@ -598,7 +599,7 @@
       Isabelle_System.make_directory(dir)
       val path = dir + doc.path.pdf
       Bytes.write(path, doc.pdf)
-      progress.echo_document("Document at " + path.absolute)
+      progress.echo("Document at " + path.absolute)
     }
 
     documents
diff -r 6f83f7892317 -r ed59a506998f src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Nov 25 12:34:08 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Nov 25 12:52:00 2020 +0100
@@ -76,7 +76,6 @@
       val session_timings = new mutable.ListBuffer[Properties.T]
       val runtime_statistics = new mutable.ListBuffer[Properties.T]
       val task_statistics = new mutable.ListBuffer[Properties.T]
-      val document_output = new mutable.ListBuffer[String]
 
       def fun(
         name: String,
@@ -228,35 +227,28 @@
       val export_errors =
         export_consumer.shutdown(close = true).map(Output.error_message_text)
 
-      val document_errors =
+      val (document_output, document_errors) =
         try {
           if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
           {
-            val document_progress =
-              new Progress {
-                override def echo(msg: String): Unit =
-                  document_output.synchronized { document_output += msg }
-                override def echo_document(msg: String): Unit =
-                  progress.echo_document(msg)
-              }
             val documents =
               using(store.open_database_context(deps.sessions_structure))(db_context =>
                 Presentation.build_documents(session_name, deps, db_context,
                   output_sources = info.document_output,
                   output_pdf = info.document_output,
-                  progress = document_progress,
-                  verbose = verbose,
-                  verbose_latex = true))
+                  progress = progress,
+                  verbose = verbose))
             using(store.open_database(session_name, output = true))(db =>
               for (doc <- documents) {
                 db.transaction {
                   Presentation.write_document(db, session_name, doc)
                 }
               })
+            (documents.flatMap(_.log_lines), Nil)
           }
-          Nil
+          (Nil, Nil)
         }
-        catch { case Exn.Interrupt.ERROR(msg) => List(msg) }
+        catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) }
 
       val result =
       {
@@ -269,7 +261,7 @@
             session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
-            document_output.toList
+            document_output
 
         val more_errors =
           Library.trim_line(stderr.toString) :: export_errors ::: document_errors