# HG changeset patch
# User wenzelm
# Date 1519059696 -3600
# Node ID 5f4448e6066280007da42926b2384adc7e9e6835
# Parent  189c68964ab28b5d08bc456e2768e3d6b33b9444
clarified modules;

diff -r 189c68964ab2 -r 5f4448e60662 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Mon Feb 19 16:24:17 2018 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Mon Feb 19 18:01:36 2018 +0100
@@ -23,6 +23,7 @@
   val trim_value: 'a lazy -> 'a lazy
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
   val map_finished: ('a -> 'b) -> 'a lazy -> 'b lazy
+  val consolidate: 'a lazy list -> 'a lazy list
   val future: Future.params -> 'a lazy -> 'a future
 end;
 
@@ -126,6 +127,19 @@
 fun map_finished f x = if is_finished x then value (f (force x)) else map f x;
 
 
+(* consolidate in parallel *)
+
+fun consolidate xs =
+  let
+    val pending =
+      xs |> map_filter (fn x => if is_pending x then SOME (fn () => force_result x) else NONE);
+    val _ =
+      if Multithreading.relevant pending then
+        ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} pending)
+      else List.app (fn e => ignore (e ())) pending;
+  in xs end;
+
+
 (* future evaluation *)
 
 fun future params x =
diff -r 189c68964ab2 -r 5f4448e60662 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Feb 19 16:24:17 2018 +0100
+++ b/src/Pure/facts.ML	Mon Feb 19 18:01:36 2018 +0100
@@ -206,16 +206,12 @@
 fun fold_static_lazy f =
   Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
 
-fun force facts =
+fun consolidate facts =
   let
     val pending =
-      (facts, []) |-> fold_static_lazy (fn (_, ths) =>
-        if Lazy.is_pending ths then cons (fn () => Lazy.force_result ths) else I);
-  in
-    if Multithreading.relevant pending then
-      ignore (Future.forked_results {name = "Facts.force", deps = []} pending)
-    else List.app (fn e => ignore (e ())) pending
-  end;
+      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_pending ths then cons ths else I);
+    val _ = Lazy.consolidate pending;
+  in facts end;
 
 fun included verbose prev_facts facts name =
   not (exists (fn prev => defined prev name) prev_facts orelse
@@ -224,14 +220,14 @@
 in
 
 fun fold_static f facts =
-  fold_static_lazy (f o apsnd Lazy.force) (tap force facts);
+  fold_static_lazy (f o apsnd Lazy.force) (consolidate facts);
 
 fun dest_static verbose prev_facts facts =
   fold_static (fn (a, ths) => included verbose prev_facts facts a ? cons (a, ths)) facts []
   |> sort_by #1;
 
 fun dest_all context verbose prev_facts facts =
-  (facts_of (tap force facts), [])
+  (facts_of (consolidate facts), [])
   |-> Name_Space.fold_table (fn (a, fact) =>
     let val ths = (case fact of Static ths => Lazy.force ths | Dynamic f => f context)
     in included verbose prev_facts facts a ? cons (a, ths) end)