# HG changeset patch # User eberlm # Date 1502191908 -7200 # Node ID 1b70820dc6ba05e4324dd4a375385d4bc24adbb9 # Parent a8b89392ecb613f5551626cc72fde1d1c5e39b6b# Parent 911f950510e028943c84b0b5cc9f7eedba444ae7 Merged diff -r a8b89392ecb6 -r 1b70820dc6ba src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Mon Aug 07 15:10:37 2017 +0200 +++ b/src/Pure/Concurrent/future.ML Tue Aug 08 13:31:48 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 a8b89392ecb6 -r 1b70820dc6ba src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Aug 07 15:10:37 2017 +0200 +++ b/src/Pure/PIDE/document.ML Tue Aug 08 13:31:48 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; diff -r a8b89392ecb6 -r 1b70820dc6ba src/Pure/PIDE/execution.ML --- a/src/Pure/PIDE/execution.ML Mon Aug 07 15:10:37 2017 +0200 +++ b/src/Pure/PIDE/execution.ML Tue Aug 08 13:31:48 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); diff -r a8b89392ecb6 -r 1b70820dc6ba src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Mon Aug 07 15:10:37 2017 +0200 +++ b/src/Pure/PIDE/protocol.ML Tue Aug 08 13:31:48 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)); diff -r a8b89392ecb6 -r 1b70820dc6ba src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Aug 07 15:10:37 2017 +0200 +++ b/src/Pure/Thy/thy_info.ML Tue Aug 08 13:31:48 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