diff options
| -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 -> () |