--- 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)
--- 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
--- 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,