more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
1.1 --- a/src/Pure/Concurrent/future.ML Fri Aug 19 12:03:44 2011 +0200
1.2 +++ b/src/Pure/Concurrent/future.ML Fri Aug 19 12:51:14 2011 +0200
1.3 @@ -174,13 +174,14 @@
1.4 (* cancellation primitives *)
1.5
1.6 fun interruptible_task f x =
1.7 - if Multithreading.available then
1.8 + (if Multithreading.available then
1.9 Multithreading.with_attributes
1.10 (if is_some (worker_task ())
1.11 then Multithreading.private_interrupts
1.12 else Multithreading.public_interrupts)
1.13 (fn _ => f x)
1.14 - else interruptible f x;
1.15 + else interruptible f x)
1.16 + before Multithreading.interrupted ();
1.17
1.18 fun cancel_now group = (*requires SYNCHRONIZED*)
1.19 Task_Queue.cancel (! queue) group;
1.20 @@ -209,9 +210,9 @@
1.21 val _ = SYNCHRONIZED "finish" (fn () =>
1.22 let
1.23 val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
1.24 - val _ = Exn.capture Multithreading.interrupted ();
1.25 + val test = Exn.capture Multithreading.interrupted ();
1.26 val _ =
1.27 - if ok then ()
1.28 + if ok andalso not (Exn.is_interrupt_exn test) then ()
1.29 else if cancel_now group then ()
1.30 else cancel_later group;
1.31 val _ = broadcast work_finished;
1.32 @@ -245,7 +246,7 @@
1.33 fun worker_loop name =
1.34 (case SYNCHRONIZED name (fn () => worker_next ()) of
1.35 NONE => ()
1.36 - | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
1.37 + | SOME work => (worker_exec work; worker_loop name));
1.38
1.39 fun worker_start name = (*requires SYNCHRONIZED*)
1.40 Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
1.41 @@ -431,8 +432,7 @@
1.42 Multithreading.with_attributes
1.43 (if interrupts
1.44 then Multithreading.private_interrupts else Multithreading.no_interrupts)
1.45 - (fn _ => Position.setmp_thread_data pos e ()) before
1.46 - Multithreading.interrupted ()) ()
1.47 + (fn _ => Position.setmp_thread_data pos e ())) ()
1.48 else Exn.interrupt_exn;
1.49 in assign_result group result res end;
1.50 in (result, job) end;
2.1 --- a/src/Pure/Isar/runtime.ML Fri Aug 19 12:03:44 2011 +0200
2.2 +++ b/src/Pure/Isar/runtime.ML Fri Aug 19 12:51:14 2011 +0200
2.3 @@ -119,7 +119,7 @@
2.4 else f x;
2.5
2.6 fun controlled_execution f x =
2.7 - ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
2.8 + (f |> debugging |> Future.interruptible_task) x;
2.9
2.10 fun toplevel_error output_exn f x = f x
2.11 handle exn =>