# HG changeset patch
# User wenzelm
# Date 1446568873 -3600
# Node ID 264c7488d532cd4f1425d94f1d74486c389cb118
# Parent  f35786faee6cd781a564c1e93f0c5b16acaf7786
prefer Isabelle/Scala Future;

diff -r f35786faee6c -r 264c7488d532 src/Pure/Concurrent/par_list.scala
--- a/src/Pure/Concurrent/par_list.scala	Tue Nov 03 16:49:44 2015 +0100
+++ b/src/Pure/Concurrent/par_list.scala	Tue Nov 03 17:41:13 2015 +0100
@@ -8,38 +8,34 @@
 package isabelle
 
 
-import java.util.concurrent.{Future => JFuture, CancellationException}
-
-
 object Par_List
 {
   def managed_results[A, B](f: A => B, xs: List[A]): List[Exn.Result[B]] =
     if (xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
     else {
-      val state = Synchronized((List.empty[JFuture[Exn.Result[B]]], false))
+      val state = Synchronized((List.empty[Future[B]], false))
 
       def cancel_other(self: Int = -1): Unit =
-        state.change { case (tasks, canceled) =>
+        state.change { case (futures, canceled) =>
           if (!canceled) {
-            for ((task, i) <- tasks.iterator.zipWithIndex if i != self)
-              task.cancel(true)
+            for ((future, i) <- futures.iterator.zipWithIndex if i != self)
+              future.cancel
           }
-          (tasks, true)
+          (futures, true)
         }
 
       try {
         state.change(_ =>
           (xs.iterator.zipWithIndex.map({ case (x, self) =>
-            Standard_Thread.submit_task {
-              val result = Exn.capture { f(x) }
-              result match { case Exn.Exn(_) => cancel_other(self) case _ => }
-              result
+            Future.fork {
+              Exn.capture { f(x) } match {
+                case Exn.Exn(exn) => cancel_other(self); throw exn
+                case Exn.Res(res) => res
+              }
             }
           }).toList, false))
 
-        state.value._1.map(future =>
-          try { future.get }
-          catch { case _: CancellationException => Exn.Exn(Exn.Interrupt()): Exn.Result[B] })
+        state.value._1.map(_.join_result)
       }
       finally { cancel_other() }
     }
@@ -65,4 +61,3 @@
   def exists[A](P: A => Boolean, xs: List[A]): Boolean = find_some(P, xs).isDefined
   def forall[A](P: A => Boolean, xs: List[A]): Boolean = !exists((x: A) => !P(x), xs)
 }
-