equal
deleted
inserted
replaced
41 fun setmp flag value f x = |
41 fun setmp flag value f x = |
42 Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
42 Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
43 let |
43 let |
44 val orig_value = ! flag; |
44 val orig_value = ! flag; |
45 val _ = flag := value; |
45 val _ = flag := value; |
46 val result = Exn.capture (restore_attributes f) x; |
46 val result = Exn.capture0 (restore_attributes f) x; |
47 val _ = flag := orig_value; |
47 val _ = flag := orig_value; |
48 in Exn.release result end) (); |
48 in Exn.release result end) (); |
49 |
49 |
50 |
50 |
51 (* weak references *) |
51 (* weak references *) |