eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;
authorwenzelm
Sat Jul 28 16:08:04 2018 +0200 (11 months ago)
changeset 686986ee53660a911
parent 68697 d81a5da01796
child 68699 b624368a302f
eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;
src/Pure/Concurrent/lazy.ML
src/Pure/facts.ML
     1.1 --- a/src/Pure/Concurrent/lazy.ML	Sat Jul 28 15:09:37 2018 +0200
     1.2 +++ b/src/Pure/Concurrent/lazy.ML	Sat Jul 28 16:08:04 2018 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4    val lazy_name: string -> (unit -> 'a) -> 'a lazy
     1.5    val lazy: (unit -> 'a) -> 'a lazy
     1.6    val peek: 'a lazy -> 'a Exn.result option
     1.7 -  val is_pending: 'a lazy -> bool
     1.8    val is_running: 'a lazy -> bool
     1.9    val is_finished: 'a lazy -> bool
    1.10    val force_result: 'a lazy -> 'a Exn.result
    1.11 @@ -54,12 +53,6 @@
    1.12  fun is_value (Value _) = true
    1.13    | is_value (Lazy _) = false;
    1.14  
    1.15 -fun is_pending (Value _) = false
    1.16 -  | is_pending (Lazy var) =
    1.17 -      (case Synchronized.value var of
    1.18 -        Expr _ => true
    1.19 -      | Result _ => false);
    1.20 -
    1.21  fun is_running (Value _) = false
    1.22    | is_running (Lazy var) =
    1.23        (case Synchronized.value var of
    1.24 @@ -128,12 +121,12 @@
    1.25  
    1.26  fun consolidate xs =
    1.27    let
    1.28 -    val pending =
    1.29 -      xs |> map_filter (fn x => if is_pending x then SOME (fn () => force_result x) else NONE);
    1.30 +    val unfinished =
    1.31 +      xs |> map_filter (fn x => if is_finished x then NONE else SOME (fn () => force_result x));
    1.32      val _ =
    1.33 -      if Future.relevant pending then
    1.34 -        ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} pending)
    1.35 -      else List.app (fn e => ignore (e ())) pending;
    1.36 +      if Future.relevant unfinished then
    1.37 +        ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} unfinished)
    1.38 +      else List.app (fn e => ignore (e ())) unfinished;
    1.39    in xs end;
    1.40  
    1.41  
     2.1 --- a/src/Pure/facts.ML	Sat Jul 28 15:09:37 2018 +0200
     2.2 +++ b/src/Pure/facts.ML	Sat Jul 28 16:08:04 2018 +0200
     2.3 @@ -208,9 +208,9 @@
     2.4  
     2.5  fun consolidate facts =
     2.6    let
     2.7 -    val pending =
     2.8 -      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_pending ths then cons ths else I);
     2.9 -    val _ = Lazy.consolidate pending;
    2.10 +    val unfinished =
    2.11 +      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_finished ths then I else cons ths);
    2.12 +    val _ = Lazy.consolidate unfinished;
    2.13    in facts end;
    2.14  
    2.15  fun included verbose prev_facts facts name =