# HG changeset patch # User wenzelm # Date 1377443062 -7200 # Node ID 5d92649a310eb79c8765ee6be0cabebe6b2415dc # Parent ee8b8dafef0ebafb0fec224011f9ef23586535ae simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML); clarified Task_Queue.group_status; tuned; diff -r ee8b8dafef0e -r 5d92649a310e src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Sun Aug 25 16:03:12 2013 +0200 +++ b/src/Pure/Concurrent/future.ML Sun Aug 25 17:04:22 2013 +0200 @@ -535,8 +535,8 @@ | SOME res => if Exn.is_interrupt_exn res then (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of - NONE => res - | SOME exn => Exn.Exn exn) + [] => res + | exns => Exn.Exn (Par_Exn.make exns)) else res); local diff -r ee8b8dafef0e -r 5d92649a310e src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Sun Aug 25 16:03:12 2013 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Sun Aug 25 17:04:22 2013 +0200 @@ -12,7 +12,7 @@ val eq_group: group * group -> bool val cancel_group: group -> exn -> unit val is_canceled: group -> bool - val group_status: group -> exn option + val group_status: group -> exn list val str_of_group: group -> string val str_of_groups: group -> string type task @@ -82,14 +82,9 @@ is_some (Synchronized.value status) orelse (case parent of NONE => false | SOME group => is_canceled group); -fun group_exns (Group {parent, status, ...}) = +fun group_status (Group {parent, status, ...}) = the_list (Synchronized.value status) @ - (case parent of NONE => [] | SOME group => group_exns group); - -fun group_status group = - (case group_exns group of - [] => NONE - | exns => SOME (Par_Exn.make exns)); + (case parent of NONE => [] | SOME group => group_status group); fun str_of_group group = (is_canceled group ? enclose "(" ")") (string_of_int (group_id group)); diff -r ee8b8dafef0e -r 5d92649a310e src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Aug 25 16:03:12 2013 +0200 +++ b/src/Pure/Thy/thy_info.ML Sun Aug 25 17:04:22 2013 +0200 @@ -174,11 +174,9 @@ fun result_commit (Result {commit, ...}) = commit; fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); -fun join_proofs (Result {theory, id, ...}) = - let - val result1 = Exn.capture Thm.join_theory_proofs theory; - val results2 = Future.join_results (Goal.peek_futures id); - in result1 :: results2 end; +fun join_theory (Result {theory, id, ...}) = + Exn.capture Thm.join_theory_proofs theory :: + map Exn.Exn (maps Task_Queue.group_status (Goal.peek_futures id)); datatype task = @@ -198,7 +196,7 @@ Task (parents, body) => let val result = body (task_parents deps parents); - val _ = Par_Exn.release_all (join_proofs result); + val _ = Par_Exn.release_all (join_theory result); val _ = result_present result (); val _ = result_commit result (); in result_theory result end @@ -224,7 +222,7 @@ val results1 = futures |> maps (fn future => (case Future.join_result future of - Exn.Res result => join_proofs result + Exn.Res result => join_theory result | Exn.Exn exn => [Exn.Exn exn])); val results2 = futures @@ -237,7 +235,7 @@ |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); (* FIXME avoid global reset_futures (!??) *) - val results4 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ())); + val results4 = map Exn.Exn (maps Task_Queue.group_status (Goal.reset_futures ())); val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); in () end); diff -r ee8b8dafef0e -r 5d92649a310e src/Pure/goal.ML --- a/src/Pure/goal.ML Sun Aug 25 16:03:12 2013 +0200 +++ b/src/Pure/goal.ML Sun Aug 25 17:04:22 2013 +0200 @@ -26,7 +26,7 @@ val norm_result: thm -> thm val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future val fork: int -> (unit -> 'a) -> 'a future - val peek_futures: int -> unit future list + val peek_futures: int -> Future.group list val purge_futures: int list -> unit val reset_futures: unit -> Future.group list val shutdown_futures: unit -> unit @@ -117,12 +117,11 @@ val forked_proofs = Synchronized.var "forked_proofs" - (Inttab.empty: (Future.group * unit future) list Inttab.table); + (Inttab.empty: Future.group list Inttab.table); fun register_forked id future = - Synchronized.change forked_proofs (fn tab => - let val group = Task_Queue.group_of_task (Future.task_of future) - in Inttab.cons_list (id, (group, Future.map (K ()) future)) tab end); + Synchronized.change forked_proofs + (Inttab.cons_list (id, Task_Queue.group_of_task (Future.task_of future))); fun status task markups = let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)] @@ -164,30 +163,28 @@ fork_params {name = "Goal.fork", pos = Position.thread_data (), pri = pri} e; fun peek_futures id = - map #2 (Inttab.lookup_list (Synchronized.value forked_proofs) id); - -fun check_canceled id group = - if Task_Queue.is_canceled group then () - else raise Fail ("Attempt to purge valid execution " ^ string_of_int id); + Inttab.lookup_list (Synchronized.value forked_proofs) id; fun purge_futures ids = Synchronized.change forked_proofs (fn tab => let val tab' = fold Inttab.delete_safe ids tab; val () = - Inttab.fold (fn (id, futures) => fn () => + Inttab.fold (fn (id, groups) => fn () => if Inttab.defined tab' id then () - else List.app (check_canceled id o #1) futures) tab (); + else groups |> List.app (fn group => + if Task_Queue.is_canceled group then () + else raise Fail ("Attempt to purge valid execution " ^ string_of_int id))) tab (); in tab' end); fun reset_futures () = Synchronized.change_result forked_proofs (fn tab => - let val groups = Inttab.fold (fold (cons o #1) o #2) tab [] + let val groups = Inttab.fold (fold cons o #2) tab [] in (groups, Inttab.empty) end); fun shutdown_futures () = (Future.shutdown (); - (case map_filter Task_Queue.group_status (reset_futures ()) of + (case maps Task_Queue.group_status (reset_futures ()) of [] => () | exns => raise Par_Exn.make exns));