# 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