diff options
author | 2003-03-27 16:18:27 +0000 | |
---|---|---|
committer | 2003-03-27 16:18:27 +0000 | |
commit | 3d29ae897bd291994a81df69096be3dfee17c418 (patch) | |
tree | 0b7badc639b243851135ad66d42d0b8c5b083b32 /ide/coqide.ml | |
parent | 8e58adef25aa61f67a36a6f4be74489efa7184a6 (diff) |
coqide: bugfix du C-C pendant Undo+paren_highlight
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3798 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r-- | ide/coqide.ml | 34 |
1 files changed, 22 insertions, 12 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 9d31a6c53..f177d1fcc 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -83,7 +83,6 @@ let get_current_tab_label () = get_tab_label (notebook())#current_page let get_current_page () = let i = (notebook())#current_page in (notebook())#get_nth_page i - let reset_tab_label i = set_tab_label i (get_tab_label i) @@ -117,7 +116,6 @@ type 'a viewable_script = } - class type analyzed_views = object('self) val mutable act_id : GtkSignal.id option @@ -177,6 +175,7 @@ object('self) method show_goals_full : unit method undo_last_step : unit method help_for_keyword : unit -> unit + method complete_at_offset : int -> unit end let (input_views:analyzed_views viewable_script Vector.t) = Vector.create () @@ -221,10 +220,6 @@ let unset_break () = let pid = Unix.getpid () let break () = Unix.kill pid Sys.sigusr1 -(* let () = Sys.set_signal Sys.sigint (Sys.Signal_handle (fun _ -> Pervasives.prerr_endline "HELLO"; - - Pervasives.flush stderr)) -*) let can_break () = set_break () let cant_break () = unset_break () @@ -554,7 +549,7 @@ object(self) ) r; ignore (proof_view#scroll_to_mark my_mark) - with e -> prerr_endline (Printexc.to_string e) + with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e) method show_goals_full = @@ -686,6 +681,7 @@ object(self) ~stop:stopi )); None + method find_phrase_starting_at (start:GText.iter) = prerr_endline "find_phrase_starting_at starting now"; let trash_bytes = ref "" in @@ -727,6 +723,9 @@ object(self) Some (start,end_iter) with _ -> None + method complete_at_offset (offset:int) = () + + method process_next_phrase display_goals do_highlight = self#clear_message; prerr_endline "process_next_phrase starting now"; @@ -899,9 +898,11 @@ object(self) let done_smthg, undos = pop_commands false (Some 0) in if done_smthg then begin - (match undos with - | None -> synchro () - | Some n -> try Pfedit.undo n with _ -> synchro ()); + try (match undos with + | None -> synchro () + | Some n -> try Pfedit.undo n with _ -> synchro ()) + with _ -> !push_info "WARNING: interrupted undo -> Coq might be in an inconsistent state. +Restart and report if you never tried to interrupt an Undo."; let start = if is_empty () then input_buffer#start_iter else input_buffer#get_iter_at_mark (top ()).stop in @@ -1157,7 +1158,7 @@ object(self) ) ); ignore (input_buffer#add_selection_clipboard (cb())); - let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "red"] in + let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "purple"] in self#electric_paren paren_highlight_tag; ignore (input_buffer#connect#after#mark_set ~callback:(fun it (m:Gtk.textmark) -> @@ -1543,7 +1544,16 @@ let main files = let search_i = edit_f#add_item "Search" ~key:GdkKeysyms._F ~callback:(fun b -> - let v = get_current_view () in () + let v = get_current_view () in + !flash_info "Search Unsupported" + ) + in + let complete_i = edit_f#add_item "Complete" + ~key:GdkKeysyms._comma + ~callback:(fun b -> + let v =out_some (get_current_view ()).analyzed_view in + v#complete_at_offset (v#get_insert#offset); + !flash_info "Complete Unsupported" ) in (* search_i#misc#set_state `INSENSITIVE;*) |