added no_interrupts;
authorwenzelm
Sun, 07 Sep 2008 17:46:41 +0200
changeset 28150 cbc2cbfc840c
parent 28149 26bd1245a46b
child 28151 61f9c918b410
added no_interrupts; tuned;
src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 07 17:46:40 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 07 17:46:41 2008 +0200
@@ -82,10 +82,11 @@
     [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]
     (fn _ => f);
 
+val no_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
+
 fun uninterruptible f =
-  with_attributes
-    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]
-    (fn atts => f (fn g => with_attributes atts (fn _ => g)));
+  with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));
 
 
 (* execution with time limit *)
@@ -193,7 +194,7 @@
 fun self_critical () =
   (case ! critical_thread of
     NONE => false
-  | SOME id => Thread.equal (id, Thread.self ()));
+  | SOME t => Thread.equal (t, Thread.self ()));
 
 fun NAMED_CRITICAL name e =
   if self_critical () then e ()