diff options
| author |  monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-18 11:28:04 +0000 |
|---|---|---|
| committer | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-18 11:28:04 +0000 |
| commit | ef1f5d8e846bb46d9e71014259365c0a16609c9a (patch) | |
| tree | f9d8ce71d427e4f0d4d6d0804691ff2d3747f6c0 | |
| parent | 6a8bc7c39cf22fda3804c0855a42e497897e9ed7 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4178 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/command_windows.ml | 9 | ||||
| -rw-r--r-- | 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 -> () |