diff -r 9f205ca4178a -r 52e43a93d51f src/Pure/General/logger.scala
--- a/src/Pure/General/logger.scala	Sun May 23 23:15:04 2021 +0200
+++ b/src/Pure/General/logger.scala	Mon May 24 11:58:06 2021 +0200
@@ -11,6 +11,9 @@
 {
   def make(log_file: Option[Path]): Logger =
     log_file match { case Some(file) => new File_Logger(file) case None => No_Logger }
+
+  def make(progress: Progress): Logger =
+    new Logger { def apply(msg: => String): Unit = progress.echo(msg) }
 }
 
 trait Logger