1.1 --- a/src/Pure/Concurrent/task_queue.ML	Wed Aug 17 20:08:36 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Wed Aug 17 22:14:22 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    val eq_group: group * group -> bool
     1.5    val cancel_group: group -> exn -> unit
     1.6    val is_canceled: group -> bool
     1.7 -  val group_status: group -> exn list
     1.8 +  val group_status: group -> exn option
     1.9    val str_of_group: group -> string
    1.10    val str_of_groups: group -> string
    1.11    type task
    1.12 @@ -56,12 +56,12 @@
    1.13  abstype group = Group of
    1.14   {parent: group option,
    1.15    id: int,
    1.16 -  status: exn list Synchronized.var}
    1.17 +  status: exn option Synchronized.var}
    1.18  with
    1.19  
    1.20  fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
    1.21  
    1.22 -fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []);
    1.23 +fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE);
    1.24  
    1.25  fun group_id (Group {id, ...}) = id;
    1.26  fun eq_group (group1, group2) = group_id group1 = group_id group2;
    1.27 @@ -74,17 +74,20 @@
    1.28  
    1.29  fun cancel_group (Group {status, ...}) exn =
    1.30    Synchronized.change status
    1.31 -    (fn exns =>
    1.32 -      if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
    1.33 -      else exns);
    1.34 +    (fn exns => SOME (Par_Exn.make (exn :: the_list exns)));
    1.35  
    1.36  fun is_canceled (Group {parent, status, ...}) =
    1.37 -  not (null (Synchronized.value status)) orelse
    1.38 +  is_some (Synchronized.value status) orelse
    1.39      (case parent of NONE => false | SOME group => is_canceled group);
    1.40  
    1.41 -fun group_status (Group {parent, status, ...}) =
    1.42 -  Synchronized.value status @
    1.43 -    (case parent of NONE => [] | SOME group => group_status group);
    1.44 +fun group_exns (Group {parent, status, ...}) =
    1.45 +  the_list (Synchronized.value status) @
    1.46 +    (case parent of NONE => [] | SOME group => group_exns group);
    1.47 +
    1.48 +fun group_status group =
    1.49 +  (case group_exns group of
    1.50 +    [] => NONE
    1.51 +  | exns => SOME (Par_Exn.make exns));
    1.52  
    1.53  fun str_of_group group =
    1.54    (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));