# HG changeset patch
# User wenzelm
# Date 1532786884 -7200
# Node ID 6ee53660a911cd5b03e2489350129578230d702f
# Parent  d81a5da01796d90cba832334ddf45bc2f4ed4cb0
eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;

diff -r d81a5da01796 -r 6ee53660a911 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Sat Jul 28 15:09:37 2018 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Sat Jul 28 16:08:04 2018 +0200
@@ -13,7 +13,6 @@
   val lazy_name: string -> (unit -> 'a) -> 'a lazy
   val lazy: (unit -> 'a) -> 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
-  val is_pending: 'a lazy -> bool
   val is_running: 'a lazy -> bool
   val is_finished: 'a lazy -> bool
   val force_result: 'a lazy -> 'a Exn.result
@@ -54,12 +53,6 @@
 fun is_value (Value _) = true
   | is_value (Lazy _) = false;
 
-fun is_pending (Value _) = false
-  | is_pending (Lazy var) =
-      (case Synchronized.value var of
-        Expr _ => true
-      | Result _ => false);
-
 fun is_running (Value _) = false
   | is_running (Lazy var) =
       (case Synchronized.value var of
@@ -128,12 +121,12 @@
 
 fun consolidate xs =
   let
-    val pending =
-      xs |> map_filter (fn x => if is_pending x then SOME (fn () => force_result x) else NONE);
+    val unfinished =
+      xs |> map_filter (fn x => if is_finished x then NONE else SOME (fn () => force_result x));
     val _ =
-      if Future.relevant pending then
-        ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} pending)
-      else List.app (fn e => ignore (e ())) pending;
+      if Future.relevant unfinished then
+        ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} unfinished)
+      else List.app (fn e => ignore (e ())) unfinished;
   in xs end;
 
 
diff -r d81a5da01796 -r 6ee53660a911 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sat Jul 28 15:09:37 2018 +0200
+++ b/src/Pure/facts.ML	Sat Jul 28 16:08:04 2018 +0200
@@ -208,9 +208,9 @@
 
 fun consolidate facts =
   let
-    val pending =
-      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_pending ths then cons ths else I);
-    val _ = Lazy.consolidate pending;
+    val unfinished =
+      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_finished ths then I else cons ths);
+    val _ = Lazy.consolidate unfinished;
   in facts end;
 
 fun included verbose prev_facts facts name =