--- a/src/Pure/Concurrent/future.ML Mon Aug 07 14:40:35 2017 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Aug 07 21:43:33 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 *)
--- a/src/Pure/PIDE/document.ML Mon Aug 07 14:40:35 2017 +0200
+++ b/src/Pure/PIDE/document.ML Mon Aug 07 21:43:33 2017 +0200
@@ -58,7 +58,7 @@
{header: node_header, (*master directory, theory header, errors*)
keywords: Keyword.keywords option, (*outer syntax keywords*)
perspective: perspective, (*command perspective*)
- entries: Command.exec option Entries.T, (*command entries with excecutions*)
+ entries: Command.exec option Entries.T, (*command entries with executions*)
result: Command.eval option} (*result of last execution*)
and version = Version of node String_Graph.T (*development graph wrt. static imports*)
with
@@ -607,8 +607,6 @@
if not proper_init andalso is_none init then NONE
else
let
- val (_, (eval, _)) = command_exec;
-
val command_visible = visible_command node command_id';
val command_overlays = overlays node command_id';
val (command_name, blob_digests, blobs_index, span0) = the_command state command_id';
@@ -616,15 +614,15 @@
val span = Lazy.force span0;
val eval' =
- Command.eval keywords (master_directory node)
- (fn () => the_default illegal_init init span) (blobs, blobs_index) span eval;
+ Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span)
+ (blobs, blobs_index) span (#1 (#2 command_exec));
val prints' =
perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
val exec' = (eval', prints');
val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
val init' = if command_name = Thy_Header.theoryN then NONE else init;
- in SOME (assign_update', (command_id', (eval', prints')), init') end;
+ in SOME (assign_update', (command_id', exec'), init') end;
fun removed_execs node0 (command_id, exec_ids) =
subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id));
@@ -679,7 +677,7 @@
SOME id => (id, the_default Command.no_exec (the_entry node id))
| NONE => (Document_ID.none, Command.init_exec ml_root));
- val (updated_execs, (command_id', (eval', _)), _) =
+ val (updated_execs, (command_id', exec'), _) =
(print_execs, common_command_exec, if initial then SOME init else NONE)
|> (still_visible orelse node_required) ?
iterate_entries_after common
@@ -698,7 +696,7 @@
if command_id' = Document_ID.none then NONE else SOME command_id';
val result =
if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
- else SOME eval';
+ else SOME (#1 exec');
val assign_update = assign_update_result assigned_execs;
val removed = maps (removed_execs node0) assign_update;
--- a/src/Pure/PIDE/execution.ML Mon Aug 07 14:40:35 2017 +0200
+++ b/src/Pure/PIDE/execution.ML Mon Aug 07 21:43:33 2017 +0200
@@ -12,6 +12,8 @@
val is_running: Document_ID.execution -> bool
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}
@@ -57,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;
@@ -69,11 +71,29 @@
val execs' = execs |> ok ? Inttab.update (exec_id, (groups, []));
in (ok, (execution_id', execs')) end);
-fun peek exec_id =
- (case Inttab.lookup (#2 (get_state ())) exec_id of
+
+(* exec groups and tasks *)
+
+fun exec_groups ((_, execs): state) exec_id =
+ (case Inttab.lookup execs exec_id of
SOME (groups, _) => groups
| NONE => []);
+fun snapshot exec_ids =
+ 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);
--- a/src/Pure/PIDE/protocol.ML Mon Aug 07 14:40:35 2017 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Aug 07 21:43:33 2017 +0200
@@ -100,7 +100,7 @@
val _ =
(singleton o Future.forks)
{name = "Document.update/remove", group = NONE,
- deps = maps Future.group_snapshot (maps Execution.peek removed),
+ deps = Execution.snapshot removed,
pri = Task_Queue.urgent_pri + 2, interrupts = false}
(fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
--- a/src/Pure/Thy/thy_info.ML Mon Aug 07 14:40:35 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Aug 07 21:43:33 2017 +0200
@@ -154,11 +154,10 @@
fun join_theory (Result {theory, exec_id, ...}) =
let
- (*toplevel proofs and diags*)
- val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek 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) |
@@ -169,8 +168,6 @@
fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
-local
-
val schedule_seq =
String_Graph.schedule (fn deps => fn (_, task) =>
(case task of
@@ -222,13 +219,6 @@
val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
in () end);
-in
-
-fun schedule_tasks tasks =
- if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks;
-
-end;
-
(* eval theory *)
@@ -403,7 +393,7 @@
let
val (_, tasks) =
require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
- in schedule_tasks tasks end;
+ in if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks end;
fun use_thy name =
use_theories