# HG changeset patch
# User wenzelm
# Date 1248212549 -7200
# Node ID 47d0da617fccd6210332b2ee4d6d00693fe63bc8
# Parent  d7697e311d8180bbead46ab390efe5d4c3498034
future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
control combinators: paranoia eta-expansion to ensure proper operational semantics;

diff -r d7697e311d81 -r 47d0da617fcc src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Jul 21 20:37:32 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Jul 21 23:42:29 2009 +0200
@@ -157,14 +157,19 @@
 fun future_job group (e: unit -> 'a) =
   let
     val result = ref (NONE: 'a Exn.result option);
-    val job = Multithreading.with_attributes Multithreading.restricted_interrupts
-      (fn _ => fn ok =>
-        let
-          val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
-          val _ = result := SOME res;
-          val _ = (case res of Exn.Exn exn => Task_Queue.cancel_group group exn | _ => ());
-          val res_ok = is_some (Exn.get_result res);
-        in res_ok end);
+    fun job ok =
+      let
+        val res =
+          if ok then
+            Multithreading.with_attributes Multithreading.restricted_interrupts
+              (fn _ => fn () => Exn.capture e ()) ()
+          else Exn.Exn Exn.Interrupt;
+        val _ = result := SOME res;
+      in
+        (case res of
+          Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
+        | Exn.Result _ => true)
+      end;
   in (result, job) end;
 
 fun do_cancel group = (*requires SYNCHRONIZED*)
@@ -203,7 +208,7 @@
     | some => some);
 
 fun worker_loop name =
-  (case SYNCHRONIZED name worker_next of
+  (case SYNCHRONIZED name (fn () => worker_next ()) of
     NONE => ()
   | SOME work => (execute name work; worker_loop name));
 
@@ -259,7 +264,7 @@
   in continue end;
 
 fun scheduler_loop () =
-  while SYNCHRONIZED "scheduler" scheduler_next do ();
+  while SYNCHRONIZED "scheduler" (fn () => scheduler_next ()) do ();
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
diff -r d7697e311d81 -r 47d0da617fcc src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Jul 21 20:37:32 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Jul 21 23:42:29 2009 +0200
@@ -92,10 +92,12 @@
     val _ = Thread.setAttributes orig_atts;
   in Exn.release result end;
 
-fun interruptible f = with_attributes regular_interrupts (fn _ => f);
+fun interruptible f =
+  with_attributes regular_interrupts (fn _ => fn x => f x);
 
 fun uninterruptible f =
-  with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));
+  with_attributes no_interrupts (fn atts => fn x =>
+    f (fn g => with_attributes atts (fn _ => fn y => g y)) x);
 
 
 (* execution with time limit *)