# HG changeset patch
# User wenzelm
# Date 1669412290 -3600
# Node ID 0bab4c7514785704b05cab3d4d54bd4f63e7f088
# Parent  cdbe200240384e43eb2c9833d3cf9090b5d2853a
clarified exception: avoid odd compiler warning;

diff -r cdbe20024038 -r 0bab4c751478 src/Pure/Concurrent/par_list.scala
--- a/src/Pure/Concurrent/par_list.scala	Fri Nov 25 21:58:40 2022 +0100
+++ b/src/Pure/Concurrent/par_list.scala	Fri Nov 25 22:38:10 2022 +0100
@@ -47,13 +47,15 @@
   def map[A, B](f: A => B, xs: List[A], sequential: Boolean = false): List[B] =
     Exn.release_first(managed_results(f, xs, sequential = sequential))
 
+  private class Found(val res: Any) extends Exception
+
   def get_some[A, B](f: A => Option[B], xs: List[A]): Option[B] = {
-    class Found(val res: B) extends Exception
     val results =
       managed_results(
         (x: A) => f(x) match { case None => () case Some(y) => throw new Found(y) }, xs)
     results.collectFirst({
-      case Exn.Exn(found) if found.isInstanceOf[Found] => found.asInstanceOf[Found].res
+      case Exn.Exn(found) if found.isInstanceOf[Found] =>
+        found.asInstanceOf[Found].res.asInstanceOf[B]
     }) match {
       case None => Exn.release_first(results); None
       case some => some