src/Pure/Concurrent/task_queue.ML
changeset 44247 270366301bd7
parent 44112 ef876972fdc1
child 44299 061599cb6eb0
equal deleted inserted replaced
44246:380a4677c55d 44247:270366301bd7
    10   val new_group: group option -> group
    10   val new_group: group option -> group
    11   val group_id: group -> int
    11   val group_id: group -> int
    12   val eq_group: group * group -> bool
    12   val eq_group: group * group -> bool
    13   val cancel_group: group -> exn -> unit
    13   val cancel_group: group -> exn -> unit
    14   val is_canceled: group -> bool
    14   val is_canceled: group -> bool
    15   val group_status: group -> exn list
    15   val group_status: group -> exn option
    16   val str_of_group: group -> string
    16   val str_of_group: group -> string
    17   val str_of_groups: group -> string
    17   val str_of_groups: group -> string
    18   type task
    18   type task
    19   val dummy_task: unit -> task
    19   val dummy_task: unit -> task
    20   val group_of_task: task -> group
    20   val group_of_task: task -> group
    54 (* groups *)
    54 (* groups *)
    55 
    55 
    56 abstype group = Group of
    56 abstype group = Group of
    57  {parent: group option,
    57  {parent: group option,
    58   id: int,
    58   id: int,
    59   status: exn list Synchronized.var}
    59   status: exn option Synchronized.var}
    60 with
    60 with
    61 
    61 
    62 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
    62 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
    63 
    63 
    64 fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []);
    64 fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE);
    65 
    65 
    66 fun group_id (Group {id, ...}) = id;
    66 fun group_id (Group {id, ...}) = id;
    67 fun eq_group (group1, group2) = group_id group1 = group_id group2;
    67 fun eq_group (group1, group2) = group_id group1 = group_id group2;
    68 
    68 
    69 fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a
    69 fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a
    72 
    72 
    73 (* group status *)
    73 (* group status *)
    74 
    74 
    75 fun cancel_group (Group {status, ...}) exn =
    75 fun cancel_group (Group {status, ...}) exn =
    76   Synchronized.change status
    76   Synchronized.change status
    77     (fn exns =>
    77     (fn exns => SOME (Par_Exn.make (exn :: the_list exns)));
    78       if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
       
    79       else exns);
       
    80 
    78 
    81 fun is_canceled (Group {parent, status, ...}) =
    79 fun is_canceled (Group {parent, status, ...}) =
    82   not (null (Synchronized.value status)) orelse
    80   is_some (Synchronized.value status) orelse
    83     (case parent of NONE => false | SOME group => is_canceled group);
    81     (case parent of NONE => false | SOME group => is_canceled group);
    84 
    82 
    85 fun group_status (Group {parent, status, ...}) =
    83 fun group_exns (Group {parent, status, ...}) =
    86   Synchronized.value status @
    84   the_list (Synchronized.value status) @
    87     (case parent of NONE => [] | SOME group => group_status group);
    85     (case parent of NONE => [] | SOME group => group_exns group);
       
    86 
       
    87 fun group_status group =
       
    88   (case group_exns group of
       
    89     [] => NONE
       
    90   | exns => SOME (Par_Exn.make exns));
    88 
    91 
    89 fun str_of_group group =
    92 fun str_of_group group =
    90   (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
    93   (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
    91 
    94 
    92 fun str_of_groups group =
    95 fun str_of_groups group =