coqide: compact delete event-search start

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3787 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 82 insertions, 18 deletions

diff --git a/ide/.coqiderc b/ide/.coqiderc
index 43883c5ff2..9983cb882b 100644
--- a/ide/.coqiderc
+++ b/ide/.coqiderc
@@ -3,7 +3,9 @@ binding "text" {
 		   "move-cursor" (display-lines,1,0)
 		   "cut-clipboard" ()	
 		}
+  bind "<ctrl>w" { "cut-clipboard" () }
   bind "<ctrl>x" { }
+
   bind "F13" {"insert-at-cursor" ("∀")}
   bind "F14" {"insert-at-cursor" ("∃")}
 }
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 01331ef9bb..6b63c788ea 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1180,7 +1180,7 @@ let main files =
   in
   let load_m = file_factory#add_item "_Open/Create" ~key:GdkKeysyms._O in
   let load_f () = 	  
-    match GToolbox.select_file ~title:"_Load file" () with 
+    match  select_file ~title:"_Load file" () with 
       | None -> ()
       | (Some f) as fn -> load f
   in
@@ -1405,7 +1405,7 @@ let main files =
 	   (fun () -> GtkSignal.emit_unit
 	      (get_current_view()).view#as_view 
 	      GtkText.View.Signals.copy_clipboard));
-  ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
+  ignore(edit_f#add_item "Cut" (* ~key:GdkKeysyms._X *) ~callback:
 	   (do_if_not_computing 
 	      (fun () -> GtkSignal.emit_unit
 		 (get_current_view()).view#as_view 
@@ -1425,6 +1425,13 @@ let main files =
 				) 
   in
   read_only_i#misc#set_state `INSENSITIVE;
+  let search_i = edit_f#add_item "Search"
+		   ~key:GdkKeysyms._F
+		   ~callback:(fun b -> 
+				let v = get_current_view () in ()
+			     ) 
+  in
+(*  search_i#misc#set_state `INSENSITIVE;*)
 
   to_do_on_page_switch := 
   (fun i -> 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index bca97c7a72..cb018e842c 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -127,3 +127,32 @@ let read_stdout,clear_stdout =
      Buffer.clear out_buff; r),
   (fun () -> 
      Format.pp_print_flush !Pp_control.std_ft (); Buffer.clear out_buff)
+
+
+let last_dir = ref ""
+let select_file ~title ?(dir = last_dir) ?(filename="") () =
+  let fs =
+    if Filename.is_relative filename then begin
+      if !dir <> "" then
+        let filename = Filename.concat !dir filename in 
+        GWindow.file_selection ~modal:true ~title ~filename ()
+      else
+        GWindow.file_selection ~modal:true ~title ()
+    end else begin
+      dir := Filename.dirname filename;
+      GWindow.file_selection ~modal:true ~title ~filename ()
+    end
+  in
+  fs#complete ~filter:"";
+  ignore (fs#connect#destroy ~callback: GMain.Main.quit);
+  let file = ref None in 
+  ignore (fs#ok_button#connect#clicked ~callback:
+    begin fun () ->
+      file := Some fs#get_filename; 
+      dir := Filename.dirname fs#get_filename;
+      fs#destroy ()
+    end);
+  ignore (fs # cancel_button # connect#clicked ~callback:fs#destroy);
+  fs # show ();
+  GMain.Main.main ();
+  !file
diff --git a/ide/undo.ml b/ide/undo.ml
index d172ec605c..ecf981c563 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -76,16 +76,19 @@ object(self)
 
   method redo = prerr_endline "REDO"; true
   initializer
+    ignore (self#buffer#connect#mark_set
+	      ~callback:
+	      (fun it tm -> if !undo_lock && not (Queue.is_empty redo) then begin
+		 Stack.iter (fun e -> Stack.push (neg e) history) nredo;
+		 Stack.clear nredo;
+		 Queue.iter (fun e -> Stack.push e history) redo;
+		 Queue.clear redo;
+	       end)
+	   );
     ignore (self#buffer#connect#insert_text 
 	      ~callback:
 	      (fun it s ->
-		 if !undo_lock && not (Queue.is_empty redo) then begin
-		   Stack.iter (fun e -> Stack.push (neg e) history) nredo;
-		   Stack.clear nredo;
-		   Queue.iter (fun e -> Stack.push e history) redo;
-		   Queue.clear redo;
-		 end;
-		   let pos = it#offset in
+		 let pos = it#offset in
 		 if Stack.is_empty history or 
 		   s=" " or s="\t" or s="\n" or
 					(match Stack.top history with 
@@ -112,13 +115,33 @@ object(self)
 		   Queue.iter (fun e -> Stack.push e history) redo;
 		   Queue.clear redo;
 		 end;
-		 Stack.push 
-		   (Delete(self#buffer#get_text ~start ~stop (),
-			   start#offset,
-			   stop#offset - start#offset
-			  ))
-		   history;
-		 self#dump_debug
+		 let start_offset = start#offset in
+		 let stop_offset = stop#offset in
+		 let s = self#buffer#get_text ~start ~stop () in
+		 if Stack.is_empty history or (match Stack.top history with
+						 | Delete(old,opos,olen) -> 
+						     olen=1 or opos <> start_offset
+						 | _ -> true
+					      )
+		 then
+		   Stack.push 
+		     (Delete(s,
+			     start_offset,
+			     stop_offset - start_offset
+			    ))
+		     history
+	       else begin
+		   match Stack.pop history with
+		     | Delete(olds,offset,len) -> 
+			 Stack.push 
+			 (Delete(olds^s,
+				 offset,
+				 len+(Glib.Utf8.length s)))
+			 history
+		     | _ -> assert false
+		 
+	       end;
+	    self#dump_debug
 	      ))
 end
 
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
index edc9d2b065..1fd15f77aa 100644
--- a/ide/utils/editable_cells.ml
+++ b/ide/utils/editable_cells.ml
@@ -1,8 +1,11 @@
+open GTree
+open Gobject
+
 let create l = 
   let hbox = GPack.hbox () in
   let columns = new GTree.column_list in
-  let command_col =  columns#add GTree.Data.string in
-  let coq_col = columns#add GTree.Data.string in
+  let command_col =  columns#add Data.string in
+  let coq_col = columns#add Data.string in
   let store = GTree.list_store columns
   in 
 (* populate the store *)