src/Pure/System/progress.scala
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)