proper sync_database for receive timeout;
authorwenzelm
Tue, 22 Aug 2023 12:18:31 +0200
changeset 78565 05de3e068312
parent 78564 8ba186dc9bc8
child 78566 a04277e3b313
proper sync_database for receive timeout;
src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue Aug 22 11:54:06 2023 +0200
+++ b/src/Pure/System/progress.scala	Tue Aug 22 12:18:31 2023 +0200
@@ -343,7 +343,11 @@
 
     _consumer = Consumer_Thread.fork_bulk[Progress.Output](name = "Database_Progress.consumer")(
       bulk = _ => true, timeout = timeout,
-      consume = bulk_output => (bulk_output.grouped(200).toList.flatMap(consume), true))
+      consume = { bulk_output =>
+        val results =
+          if (bulk_output.isEmpty) consume(Nil)
+          else bulk_output.grouped(200).toList.flatMap(consume)
+        (results, true) })
   }
 
   def exit(close: Boolean = false): Unit = synchronized {