equal
deleted
inserted
replaced
37 |
37 |
38 val available = false; |
38 val available = false; |
39 val max_threads = ref (1: int); |
39 val max_threads = ref (1: int); |
40 fun max_threads_value () = Int.max (! max_threads, 1); |
40 fun max_threads_value () = Int.max (! max_threads, 1); |
41 |
41 |
42 val no_interrupts = []; |
42 val no_interrupts = |
43 val regular_interrupts = []; |
43 [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]; |
|
44 |
|
45 val regular_interrupts = |
|
46 [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]; |
44 |
47 |
45 fun with_attributes _ f x = f [] x; |
48 fun with_attributes _ f x = f [] x; |
46 |
49 |
47 |
50 |
48 (* critical section *) |
51 (* critical section *) |