# HG changeset patch
# User wenzelm
# Date 1605817392 -3600
# Node ID e9030100f97da0be461f8b23e8c059e3983aa3bc
# Parent  5c08ad7adf778fb2a41e51d7f585edacdd8c62e4
clarified signature;

diff -r 5c08ad7adf77 -r e9030100f97d src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu Nov 19 21:12:35 2020 +0100
+++ b/src/Pure/System/progress.scala	Thu Nov 19 21:23:12 2020 +0100
@@ -32,7 +32,7 @@
 
   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(path: Path) { echo("Document at " + path.absolute) }
+  def echo_document(msg: String) { echo(Output.error_message_text(msg)) }
 
   def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
     Timing.timeit(message, enabled, echo)(e)
diff -r 5c08ad7adf77 -r e9030100f97d src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Nov 19 21:12:35 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 19 21:23:12 2020 +0100
@@ -511,7 +511,7 @@
     for (dir <- doc_output; (doc, pdf) <- documents) {
       val path = dir + doc.path.pdf
       Bytes.write(path, pdf)
-      progress.echo_document(path)
+      progress.echo_document("Document at " + path.absolute)
     }
 
     documents
diff -r 5c08ad7adf77 -r e9030100f97d src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Nov 19 21:12:35 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Nov 19 21:23:12 2020 +0100
@@ -225,8 +225,8 @@
                   new Progress {
                     override def echo(msg: String): Unit =
                       document_output.synchronized { document_output += msg }
-                    override def echo_document(path: Path): Unit =
-                      progress.echo_document(path)
+                    override def echo_document(msg: String): Unit =
+                      progress.echo_document(msg)
                   }
                 val documents =
                   Presentation.build_documents(session_name, deps, store, verbose = verbose,