clarified exception: avoid odd compiler warning;
authorwenzelm
Fri, 25 Nov 2022 22:38:10 +0100
changeset 76538 0bab4c751478
parent 76537 cdbe20024038
child 76539 8c94ca4dd035
clarified exception: avoid odd compiler warning;
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