equal
deleted
inserted
replaced
25 fun interrupt thread = Thread.interrupt thread handle Thread _ => (); |
25 fun interrupt thread = Thread.interrupt thread handle Thread _ => (); |
26 |
26 |
27 |
27 |
28 (* basic synchronization *) |
28 (* basic synchronization *) |
29 |
29 |
30 fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () => |
30 fun synchronized name lock e = |
31 let |
31 if Multithreading.available then |
32 val immediate = |
32 Exn.release (uninterruptible (fn restore_attributes => fn () => |
33 if Mutex.trylock lock then true |
33 let |
34 else |
34 val immediate = |
35 let |
35 if Mutex.trylock lock then true |
36 val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ..."); |
36 else |
37 val time = Multithreading.real_time Mutex.lock lock; |
37 let |
38 val _ = Multithreading.tracing_time true time |
38 val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ..."); |
39 (fn () => name ^ ": locked after " ^ Time.toString time); |
39 val time = Multithreading.real_time Mutex.lock lock; |
40 in false end; |
40 val _ = Multithreading.tracing_time true time |
41 val result = Exn.capture (restore_attributes e) (); |
41 (fn () => name ^ ": locked after " ^ Time.toString time); |
42 val _ = |
42 in false end; |
43 if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ..."); |
43 val result = Exn.capture (restore_attributes e) (); |
44 val _ = Mutex.unlock lock; |
44 val _ = |
45 in result end) ()); |
45 if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ..."); |
|
46 val _ = Mutex.unlock lock; |
|
47 in result end) ()) |
|
48 else e (); |
46 |
49 |
47 end; |
50 end; |