# HG changeset patch # User wenzelm # Date 1528200471 -7200 # Node ID 1b0ce345d3c846b515cf88305eb8fc49fbaa3fdc # Parent 22680a3f834635a4552ee975eae875bcb352f748 tuned; diff -r 22680a3f8346 -r 1b0ce345d3c8 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Tue Jun 05 00:06:23 2018 +0200 +++ b/src/Pure/Concurrent/future.ML Tue Jun 05 14:07:51 2018 +0200 @@ -692,9 +692,10 @@ (* snapshot: current tasks of groups *) -fun snapshot groups = - SYNCHRONIZED "snapshot" (fn () => - Task_Queue.group_tasks (! queue) groups); +fun snapshot [] = [] + | snapshot groups = + SYNCHRONIZED "snapshot" (fn () => + Task_Queue.group_tasks (! queue) groups); (* shutdown *) diff -r 22680a3f8346 -r 1b0ce345d3c8 src/Pure/PIDE/execution.ML --- a/src/Pure/PIDE/execution.ML Tue Jun 05 00:06:23 2018 +0200 +++ b/src/Pure/PIDE/execution.ML Tue Jun 05 14:07:51 2018 +0200 @@ -115,8 +115,10 @@ SOME (groups, _) => groups | NONE => []); -fun snapshot exec_ids = - change_state_result (`(fn (_, _, execs) => Future.snapshot (maps (exec_groups execs) exec_ids))); +fun snapshot [] = [] + | snapshot exec_ids = + change_state_result + (`(fn (_, _, execs) => Future.snapshot (maps (exec_groups execs) exec_ids))); fun join exec_ids = (case snapshot exec_ids of