# HG changeset patch # User wenzelm # Date 1502129123 -7200 # Node ID 6ce1afc0104094952c6a022d101a4a24b7fe44e2 # Parent de9c6560c221aea2cede3d35ad488ea897d90e2d more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids; diff -r de9c6560c221 -r 6ce1afc01040 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Mon Aug 07 15:13:21 2017 +0200 +++ b/src/Pure/Concurrent/future.ML Mon Aug 07 20:05:23 2017 +0200 @@ -31,7 +31,6 @@ val join_result: 'a future -> 'a Exn.result val joins: 'a future list -> 'a list val join: 'a future -> 'a - val join_tasks: task list -> unit val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b val value_result: 'a Exn.result -> 'a future val value: 'a -> 'a future @@ -532,14 +531,6 @@ fun joins xs = Par_Exn.release_all (join_results xs); fun join x = Exn.release (join_result x); -fun join_tasks tasks = - if null tasks then () - else - (singleton o forks) - {name = "join_tasks", group = SOME (new_group NONE), - deps = tasks, pri = 0, interrupts = false} I - |> join; - (* task context for running thread *) diff -r de9c6560c221 -r 6ce1afc01040 src/Pure/PIDE/execution.ML --- a/src/Pure/PIDE/execution.ML Mon Aug 07 15:13:21 2017 +0200 +++ b/src/Pure/PIDE/execution.ML Mon Aug 07 20:05:23 2017 +0200 @@ -13,6 +13,7 @@ val is_running_exec: Document_ID.exec -> bool val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool val snapshot: Document_ID.exec list -> Future.task list + val join: Document_ID.exec list -> unit val peek: Document_ID.exec -> Future.group list val cancel: Document_ID.exec -> unit type params = {name: string, pos: Position.T, pri: int} @@ -58,7 +59,7 @@ fun is_running execution_id = execution_id = #1 (get_state ()); -(* execs *) +(* running execs *) fun is_running_exec exec_id = Inttab.defined (#2 (get_state ())) exec_id; @@ -70,6 +71,9 @@ val execs' = execs |> ok ? Inttab.update (exec_id, (groups, [])); in (ok, (execution_id', execs')) end); + +(* exec groups and tasks *) + fun exec_groups ((_, execs): state) exec_id = (case Inttab.lookup execs exec_id of SOME (groups, _) => groups @@ -79,6 +83,15 @@ change_state_result (fn state => (maps Future.group_snapshot (maps (exec_groups state) exec_ids), state)); +fun join exec_ids = + (case snapshot exec_ids of + [] => () + | tasks => + ((singleton o Future.forks) + {name = "Execution.join", group = SOME (Future.new_group NONE), + deps = tasks, pri = 0, interrupts = false} I + |> Future.join; join exec_ids)); + fun peek exec_id = exec_groups (get_state ()) exec_id; fun cancel exec_id = List.app Future.cancel_group (peek exec_id); diff -r de9c6560c221 -r 6ce1afc01040 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Aug 07 15:13:21 2017 +0200 +++ b/src/Pure/Thy/thy_info.ML Mon Aug 07 20:05:23 2017 +0200 @@ -154,11 +154,10 @@ fun join_theory (Result {theory, exec_id, ...}) = let - (*toplevel proofs and diags*) - val _ = Future.join_tasks (Execution.snapshot [exec_id]); - (*fully nested proofs*) + val _ = Execution.join [exec_id]; val res = Exn.capture Thm.consolidate_theory theory; - in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end; + val errs = maps Task_Queue.group_status (Execution.peek exec_id); + in res :: map Exn.Exn errs end; datatype task = Task of Path.T * string list * (theory list -> result) |