Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Concurrent/lazy.ML
changeset 78766 5578341489cb
parent 78757 a094bf81a496
child 80809 4a64fc4d1cde 
--- a/src/Pure/Concurrent/lazy.ML	Thu Oct 12 15:45:06 2023 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Oct 12 14:59:59 2023 +0200
@@ -61,7 +61,7 @@
       | Result res => not (Future.is_finished res));
 
 fun is_finished_future res =
-  Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res));
+  Future.is_finished res andalso not (Exn.is_interrupt_proper_exn (Future.join_result res));
 
 fun is_finished (Value _) = true
   | is_finished (Lazy var) =
@@ -105,7 +105,7 @@
                     val _ = Exn.capture_body (fn () => Future.fulfill_result x res0);
                     val res = Future.get_result x;
                     val _ =
-                      if not (Exn.is_interrupt_exn res) then
+                      if not (Exn.is_interrupt_proper_exn res) then
                         Synchronized.assign var (Result (Future.value_result res))
                       else if strict then
                         Synchronized.assign var
isabelle