more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
authorwenzelm
Tue, 09 Feb 2021 15:40:23 +0100
changeset 73491 f69cbb59813e
parent 73490 5bded25065f8
child 73492 b9c480878663
more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
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