*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4178 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 7 insertions, 6 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 1fe1fd90b..904b08c63 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -69,12 +69,15 @@ object(self)
     let combo = GEdit.combo ~popdown_strings:Coq_commands.state_preserving
 		  ~use_arrows:`DEFAULT
 		  ~ok_if_empty:false
-		  ~value_in_list:true
+		  ~value_in_list:false (* true is not ok with disable_activate...*)
 		  ~packing:hbox#pack
 		  ()
     in
     combo#disable_activate ();
-    let on_activate c () = if List.mem combo#entry#text Coq_commands.state_preserving then c () in
+    let on_activate c () = 
+      if List.mem combo#entry#text Coq_commands.state_preserving then c () 
+      else prerr_endline "Not a state preserving command" 
+    in
     let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in
     entry#misc#set_can_default true;
     let r_bin =
@@ -111,7 +114,7 @@ object(self)
       | None , Some t -> 
 	  entry#set_text t
     end;
-    callback ();
+    on_activate callback ();
     entry#misc#grab_focus ();
     entry#misc#grab_default ();
     ignore (entry#connect#activate ~callback);
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 22aa9a41b..ee53103d8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -273,12 +273,10 @@ let full_do_if_not_computing f x =
 				f x;
 				Glib.Timeout.remove idle;
 			    prerr_endline "Releasing lock";
-			    Mutex.unlock w#lock;
 			    Mutex.unlock coq_computing;
 			      with e -> 
 				Glib.Timeout.remove idle;
 				prerr_endline "Releasing lock (on error)";
-				Mutex.unlock w#lock;
 				Mutex.unlock coq_computing;
 				raise e
 			    end
@@ -475,7 +473,7 @@ let update_on_end_of_proof id =
 	prerr_endline "Toggling Changing Reset id"; 
 	r := false
       end
-  | { ast = _, (VernacAbort _ | VernacAbortAll | VernacGoal _) } -> raise Exit
+  | { ast = _, (VernacAbort _ | VernacAbortAll | VernacGoal_) } -> raise Exit
   | _ -> ()
   in
   try Stack.iter lookup_lemma processed_stack with Exit -> ()