changeset 72574 | d892f6d66402 |
parent 71726 | a5fda30edae2 |
child 72599 | 76550282267f |
--- a/src/Pure/System/progress.scala Wed Nov 11 20:58:36 2020 +0100 +++ b/src/Pure/System/progress.scala Wed Nov 11 21:00:14 2020 +0100 @@ -32,6 +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 timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = Timing.timeit(message, enabled, echo)(e)