more robust interrupt handling as in Future.forked_results (amending 64df1e514005);

--- 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