# HG changeset patch
# User wenzelm
# Date 1692277938 -7200
# Node ID dd0501accda87c95b19d74f5d40a5e1ec411c0dc
# Parent  62c6164f0fc1e5ecc59309a59e3172111b906371
tuned;

diff -r 62c6164f0fc1 -r dd0501accda8 src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Thu Aug 17 14:46:24 2023 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Thu Aug 17 15:12:18 2023 +0200
@@ -25,7 +25,7 @@
     def consume_single(args: List[A]): (List[Exn.Result[Unit]], Boolean) = {
       assert(args.length == 1)
       Exn.capture { consume(args.head) } match {
-        case Exn.Res(continue) => (List(Exn.Res(())), continue)
+        case Exn.Res(cont) => (List(Exn.Res(())), cont)
         case Exn.Exn(exn) => (List(Exn.Exn(exn)), true)
       }
     }
@@ -88,7 +88,7 @@
             .getOrElse(msgs.take(1))
             .map(_.get)
 
-        val (results, continue) = consume(reqs.map(_.arg))
+        val (results, cont) = consume(reqs.map(_.arg))
 
         for {
           (Some(req), Some(res)) <- reqs.map(Some(_)).zipAll(results.map(Some(_)), None, None)
@@ -100,7 +100,7 @@
           }
         }
 
-        if (continue) main_loop(msgs.drop(reqs.length))
+        if (cont) main_loop(msgs.drop(reqs.length))
         else robust_finish()
     }