# HG changeset patch
# User wenzelm
# Date 1312986279 -7200
# Node ID 64634a9ecd466ef9e957123b64efa0ed519eddc2
# Parent  0baa8bbd355af59154c2574ea8348b0fb59e1232
Goal.forked: clarified handling of interrupts;

diff -r 0baa8bbd355a -r 64634a9ecd46 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Aug 10 16:05:14 2011 +0200
+++ b/src/Pure/goal.ML	Wed Aug 10 16:24:39 2011 +0200
@@ -125,12 +125,10 @@
       val _ = forked 1;
       val future =
         singleton
-          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = true})
+          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
           (fn () =>
-            (*interruptible*)
             Exn.release
-              (Exn.capture Future.status e before forked ~1
-                handle exn => (forked ~1; reraise exn)));
+              (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
     in future end) ();
 
 fun fork e = fork_name "Goal.fork" e;