# 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 *)