# HG changeset patch # User wenzelm # Date 1419765481 -3600 # Node ID 682aa538c5c088a2c1461cfacf6728023abd3d03 # Parent 3a594fd13ca4ff44359d44812040b8707c72957e more thorough Lazy.is_finished; diff -r 3a594fd13ca4 -r 682aa538c5c0 src/Pure/Concurrent/lazy.ML --- a/src/Pure/Concurrent/lazy.ML Sun Dec 28 15:42:34 2014 +1100 +++ b/src/Pure/Concurrent/lazy.ML Sun Dec 28 12:18:01 2014 +0100 @@ -36,11 +36,15 @@ Expr _ => NONE | Result res => Future.peek res); +fun is_finished (Lazy var) = + (case Synchronized.value var of + Expr _ => false + | Result res => + Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))); + fun lazy e = Lazy (Synchronized.var "lazy" (Expr e)); fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a))); -fun is_finished x = is_some (peek x); - (* force result *)