From ef1f5d8e846bb46d9e71014259365c0a16609c9a Mon Sep 17 00:00:00 2001 From: monate Date: Wed, 18 Jun 2003 11:28:04 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4178 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/command_windows.ml | 9 ++++++--- ide/coqide.ml | 4 +--- 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 -> () -- cgit v1.2.3