77 |
77 |
78 (* synchronized evaluation *) |
78 (* synchronized evaluation *) |
79 |
79 |
80 fun synchronized name lock e = |
80 fun synchronized name lock e = |
81 Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
81 Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
82 let |
82 if ! trace > 0 then |
83 val immediate = |
83 let |
84 if Mutex.trylock lock then true |
84 val immediate = |
85 else |
85 if Mutex.trylock lock then true |
86 let |
86 else |
87 val _ = tracing 5 (fn () => name ^ ": locking ..."); |
87 let |
88 val timer = Timer.startRealTimer (); |
88 val _ = tracing 5 (fn () => name ^ ": locking ..."); |
89 val _ = Mutex.lock lock; |
89 val timer = Timer.startRealTimer (); |
90 val time = Timer.checkRealTimer timer; |
90 val _ = Mutex.lock lock; |
91 val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time); |
91 val time = Timer.checkRealTimer timer; |
92 in false end; |
92 val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time); |
93 val result = Exn.capture (restore_attributes e) (); |
93 in false end; |
94 val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ..."); |
94 val result = Exn.capture (restore_attributes e) (); |
95 val _ = Mutex.unlock lock; |
95 val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ..."); |
96 in result end) ()); |
96 val _ = Mutex.unlock lock; |
|
97 in result end |
|
98 else |
|
99 let |
|
100 val _ = Mutex.lock lock; |
|
101 val result = Exn.capture (restore_attributes e) (); |
|
102 val _ = Mutex.unlock lock; |
|
103 in result end) ()); |
97 |
104 |
98 end; |
105 end; |