# HG changeset patch
# User wenzelm
# Date 1698917008 -3600
# Node ID 162ce304955e3a29b001d51289ce62de53fa8ef7
# Parent  0c7419d3dd597d9acdf3c59dedccd790280f4a97
more robust: support concurrent output;

diff -r 0c7419d3dd59 -r 162ce304955e src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu Nov 02 10:12:12 2023 +0100
+++ b/src/Pure/System/progress.scala	Thu Nov 02 10:23:28 2023 +0100
@@ -243,18 +243,20 @@
 
 class Console_Progress(override val verbose: Boolean = false, stderr: Boolean = false)
 extends Progress {
-  override def output(message: Progress.Message): Unit =
+  override def output(message: Progress.Message): Unit = synchronized {
     if (do_output(message)) {
       Output.output(message.output_text, stdout = !stderr, include_empty = true)
     }
+  }
 
   override def toString: String = super.toString + ": console"
 }
 
 class File_Progress(path: Path, override val verbose: Boolean = false)
 extends Progress {
-  override def output(message: Progress.Message): Unit =
+  override def output(message: Progress.Message): Unit = synchronized {
     if (do_output(message)) File.append(path, message.output_text + "\n")
+  }
 
   override def toString: String = super.toString + ": " + path.toString
 }