tuned;
authorwenzelm
Thu, 17 Aug 2023 15:12:18 +0200
changeset 78533 dd0501accda8
parent 78532 62c6164f0fc1
child 78534 879e1ba3868b
tuned;
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()
     }