tuned;
authorwenzelm
Tue Jun 05 14:07:51 2018 +0200 (13 months ago)
changeset 683791b0ce345d3c8
parent 68378 22680a3f8346
child 68380 f249e1f5623b
tuned;
src/Pure/Concurrent/future.ML
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jun 05 00:06:23 2018 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jun 05 14:07:51 2018 +0200
     1.3 @@ -692,9 +692,10 @@
     1.4  
     1.5  (* snapshot: current tasks of groups *)
     1.6  
     1.7 -fun snapshot groups =
     1.8 -  SYNCHRONIZED "snapshot" (fn () =>
     1.9 -    Task_Queue.group_tasks (! queue) groups);
    1.10 +fun snapshot [] = []
    1.11 +  | snapshot groups =
    1.12 +      SYNCHRONIZED "snapshot" (fn () =>
    1.13 +        Task_Queue.group_tasks (! queue) groups);
    1.14  
    1.15  
    1.16  (* shutdown *)
     2.1 --- a/src/Pure/PIDE/execution.ML	Tue Jun 05 00:06:23 2018 +0200
     2.2 +++ b/src/Pure/PIDE/execution.ML	Tue Jun 05 14:07:51 2018 +0200
     2.3 @@ -115,8 +115,10 @@
     2.4      SOME (groups, _) => groups
     2.5    | NONE => []);
     2.6  
     2.7 -fun snapshot exec_ids =
     2.8 -  change_state_result (`(fn (_, _, execs) => Future.snapshot (maps (exec_groups execs) exec_ids)));
     2.9 +fun snapshot [] = []
    2.10 +  | snapshot exec_ids =
    2.11 +      change_state_result
    2.12 +        (`(fn (_, _, execs) => Future.snapshot (maps (exec_groups execs) exec_ids)));
    2.13  
    2.14  fun join exec_ids =
    2.15    (case snapshot exec_ids of