diff options
| author | gmelquio | 2010-12-14 13:44:04 +0000 |
|---|---|---|
| committer | gmelquio | 2010-12-14 13:44:04 +0000 |
| commit | 5ea04979005e71ae5a5e8d74c29a6e7980bdcc07 (patch) | |
| tree | 5fddc1637c33cebbc848ae777255aee3fb842285 | |
| parent | 0bbe049656f4a400f65e7ef55345735148812508 (diff) | |
Fix mutex being released from a different thread than it is acquired from.
Needed for FreeBSD. Patch by Cedric Auger.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13712 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/coqide.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 0f535cfef9..9838b7c24f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -231,8 +231,9 @@ let break () = end let do_if_not_computing text f x = - if Mutex.try_lock coq_computing then - let threaded_task () = + let threaded_task () = + if Mutex.try_lock coq_computing then + begin prerr_endline "Getting lock"; List.iter (fun elt -> try f elt with @@ -247,6 +248,10 @@ let do_if_not_computing text f x = x; prerr_endline "Releasing lock"; Mutex.unlock coq_computing; + end + else + prerr_endline + "Discarded order (computations are ongoing)" in prerr_endline ("Launching thread " ^ text); ignore (Glib.Timeout.add ~ms:300 ~callback: @@ -254,9 +259,6 @@ let do_if_not_computing text f x = then (Mutex.unlock coq_computing; false) else (pbar#pulse (); true))); ignore (Thread.create threaded_task ()) - else - prerr_endline - "Discarded order (computations are ongoing)" let warning msg = GToolbox.message_box ~title:"Warning" |