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

2 files changed, 28 insertions, 13 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 9538334397..c31306131d 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -126,7 +126,9 @@ let interp_last last =
   try
     vernac_com (States.with_heavy_rollback Vernacentries.interp) last
   with e ->
-    let s,_ = process_exn e in prerr_endline s; raise e
+    let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s);
+    raise e
+
 
 (* type hyp = (identifier * constr option * constr) * string*)
 type hyp = env * evar_map *
@@ -245,6 +247,9 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
    ("Apply "^ident),
    ("Apply "^ident^".");
    
+   ("Exact "^ident),
+   ("Exact "^ident^".");
+
    ("Generalize "^ident),
    ("Generalize "^ident^".");
    
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 9d31a6c536..f177d1fcc3 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;*)