From 5ea04979005e71ae5a5e8d74c29a6e7980bdcc07 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Tue, 14 Dec 2010 13:44:04 +0000
Subject: 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
---
 ide/coqide.ml | 12 +++++++-----
 1 file 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"
-- 
cgit v1.2.3