src/Pure/Concurrent/lazy.ML
changeset 68867 a8728e3f9822
parent 68698 6ee53660a911
child 68868 5f44ad150ed8
     1.1 --- a/src/Pure/Concurrent/lazy.ML	Sat Sep 01 13:38:44 2018 +0200
     1.2 +++ b/src/Pure/Concurrent/lazy.ML	Sat Sep 01 14:25:03 2018 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    val peek: 'a lazy -> 'a Exn.result option
     1.5    val is_running: 'a lazy -> bool
     1.6    val is_finished: 'a lazy -> bool
     1.7 +  val finished_result: 'a lazy -> 'a Exn.result
     1.8    val force_result: 'a lazy -> 'a Exn.result
     1.9    val force: 'a lazy -> 'a
    1.10    val force_value: 'a lazy -> 'a lazy
    1.11 @@ -59,12 +60,22 @@
    1.12          Expr _ => false
    1.13        | Result res => not (Future.is_finished res));
    1.14  
    1.15 +fun is_finished_future res =
    1.16 +  Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res));
    1.17 +
    1.18  fun is_finished (Value _) = true
    1.19    | is_finished (Lazy var) =
    1.20        (case Synchronized.value var of
    1.21          Expr _ => false
    1.22 -      | Result res =>
    1.23 -          Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res)));
    1.24 +      | Result res => is_finished_future res);
    1.25 +
    1.26 +fun finished_result (Value a) = Exn.Res a
    1.27 +  | finished_result (Lazy var) =
    1.28 +      let fun fail () = Exn.Exn (Fail "Unfinished lazy") in
    1.29 +        (case Synchronized.value var of
    1.30 +          Expr _ => fail ()
    1.31 +        | Result res => if is_finished_future res then Future.join_result res else fail ())
    1.32 +      end;
    1.33  
    1.34  
    1.35  (* force result *)