# HG changeset patch
# User wenzelm
# Date 1612881623 -3600
# Node ID f69cbb59813ece0a3e4ff7f0b770c65a50493a63
# Parent  5bded25065f80125af8b09cbcf82798e4eef137f
more robust interrupt handling as in Future.forked_results (amending 64df1e514005);

diff -r 5bded25065f8 -r f69cbb59813e src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Tue Feb 09 14:55:36 2021 +0100
+++ b/src/Pure/System/scala.ML	Tue Feb 09 15:40:23 2021 +0100
@@ -53,11 +53,11 @@
             (case Symtab.lookup tab id of
               SOME (Exn.Exn Match) => NONE
             | SOME result => SOME (result, Symtab.delete id tab)
-            | NONE => SOME (Exn.Exn Exn.Interrupt, tab)))
-        handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn);
+            | NONE => SOME (Exn.Exn Exn.Interrupt, tab)));
     in
       invoke ();
       Exn.release (restore_attributes await_result ())
+        handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
     end) ();
 
 in