--- a/src/Pure/Concurrent/future.ML Sat Apr 09 14:00:23 2016 +0200
+++ b/src/Pure/Concurrent/future.ML Sat Apr 09 14:11:31 2016 +0200
@@ -211,7 +211,7 @@
then Thread_Attributes.private_interrupts
else Thread_Attributes.public_interrupts)
(fn _ => f x)
- before Multithreading.interrupted ();
+ before Thread_Attributes.expose_interrupt ();
(* worker threads *)
@@ -231,7 +231,7 @@
val _ = SYNCHRONIZED "finish" (fn () =>
let
val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
- val test = Exn.capture Multithreading.interrupted ();
+ val test = Exn.capture Thread_Attributes.expose_interrupt ();
val _ =
if ok andalso not (Exn.is_interrupt_exn test) then ()
else if null (cancel_now group) then ()