1.1 --- a/src/Pure/Concurrent/future.ML	Thu Sep 09 11:05:52 2010 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Sep 09 17:20:27 2010 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4      val _ = Single_Assignment.assign result res
     1.5        handle exn as Fail _ =>
     1.6          (case Single_Assignment.peek result of
     1.7 -          SOME (Exn.Exn Exn.Interrupt) => raise Exn.Interrupt
     1.8 +          SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
     1.9          | _ => reraise exn);
    1.10      val ok =
    1.11        (case the (Single_Assignment.peek result) of
    1.12 @@ -184,7 +184,7 @@
    1.13              Exn.capture (fn () =>
    1.14                Multithreading.with_attributes Multithreading.private_interrupts
    1.15                  (fn _ => Position.setmp_thread_data pos e ())) ()
    1.16 -          else Exn.Exn Exn.Interrupt;
    1.17 +          else Exn.interrupt_exn;
    1.18        in assign_result group result res end;
    1.19    in (result, job) end;
    1.20  
    1.21 @@ -359,10 +359,12 @@
    1.22  
    1.23      val _ = broadcast scheduler_event;
    1.24    in continue end
    1.25 -  handle Exn.Interrupt =>
    1.26 -   (Multithreading.tracing 1 (fn () => "Interrupt");
    1.27 -    List.app cancel_later (Task_Queue.cancel_all (! queue));
    1.28 -    broadcast_work (); true);
    1.29 +  handle exn =>
    1.30 +    if Exn.is_interrupt exn then
    1.31 +     (Multithreading.tracing 1 (fn () => "Interrupt");
    1.32 +      List.app cancel_later (Task_Queue.cancel_all (! queue));
    1.33 +      broadcast_work (); true)
    1.34 +    else reraise exn;
    1.35  
    1.36  fun scheduler_loop () =
    1.37    while
    1.38 @@ -415,11 +417,12 @@
    1.39  fun get_result x =
    1.40    (case peek x of
    1.41      NONE => Exn.Exn (Fail "Unfinished future")
    1.42 -  | SOME (exn as Exn.Exn Exn.Interrupt) =>
    1.43 -      (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
    1.44 -        [] => exn
    1.45 -      | exns => Exn.Exn (Exn.EXCEPTIONS exns))
    1.46 -  | SOME res => res);
    1.47 +  | SOME res =>
    1.48 +      if Exn.is_interrupt_exn res then
    1.49 +        (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
    1.50 +          [] => res
    1.51 +        | exns => Exn.Exn (Exn.EXCEPTIONS exns))
    1.52 +      else res);
    1.53  
    1.54  fun join_next deps = (*requires SYNCHRONIZED*)
    1.55    if null deps then NONE
    1.56 @@ -486,7 +489,7 @@
    1.57  fun promise_group group : 'a future =
    1.58    let
    1.59      val result = Single_Assignment.var "promise" : 'a result;
    1.60 -    fun abort () = assign_result group result (Exn.Exn Exn.Interrupt) handle Fail _ => true;
    1.61 +    fun abort () = assign_result group result Exn.interrupt_exn handle Fail _ => true;
    1.62      val task = SYNCHRONIZED "enqueue_passive" (fn () =>
    1.63        Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
    1.64    in Future {promised = true, task = task, group = group, result = result} end;
    1.65 @@ -496,7 +499,7 @@
    1.66  fun fulfill_result (Future {promised, task, group, result}) res =
    1.67    let
    1.68      val _ = promised orelse raise Fail "Not a promised future";
    1.69 -    fun job ok = assign_result group result (if ok then res else Exn.Exn Exn.Interrupt);
    1.70 +    fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn);
    1.71      val _ = execute (task, group, [job]);
    1.72    in () end;
    1.73