Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 05 Jun 2018 14:07:51 +0200
changeset 68379 1b0ce345d3c8
parent 68378 22680a3f8346
child 68380 f249e1f5623b
tuned;
src/Pure/Concurrent/future.ML file | annotate | diff | comparison | revisions
src/Pure/PIDE/execution.ML file | annotate | diff | comparison | revisions 
--- 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 *)
--- 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
isabelle