# HG changeset patch
# User wenzelm
# Date 1220818815 -7200
# Node ID 7718587e510e4be57887f5bc57fdadd1ef479c3c
# Parent  e0177b67ecd9dbb97c13420306290c58631fd37f
added sync_interrupts, regular_interrupts;
max_thread_value: enforce >= 1;

diff -r e0177b67ecd9 -r 7718587e510e src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 07 22:20:11 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 07 22:20:15 2008 +0200
@@ -43,7 +43,7 @@
 
 fun max_threads_value () =
   let val m = ! max_threads
-  in if m <= 0 then Thread.numProcessors () else m end;
+  in if m <= 0 then Int.max (Thread.numProcessors (), 1) else m end;
 
 
 (* misc utils *)
@@ -62,6 +62,15 @@
 
 (* thread attributes *)
 
+val no_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
+
+val sync_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
+
+val regular_interrupts =
+  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
+
 fun with_attributes new_atts f x =
   let
     val orig_atts = Thread.getAttributes ();
@@ -77,13 +86,7 @@
       handle Interrupt => (restore (); Exn.Exn Interrupt))
   end;
 
-fun interruptible f =
-  with_attributes
-    [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]
-    (fn _ => f);
-
-val no_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
+fun interruptible f = with_attributes regular_interrupts (fn _ => f);
 
 fun uninterruptible f =
   with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));