coqide: search forward

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

6 files changed, 171 insertions, 90 deletions

diff --git a/INSTALL.ide b/INSTALL.ide
index 6e471348e..4d2b123d8 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -30,7 +30,7 @@ INSTALLATION
 	If this not the case, this means that Coq computations will be
 	slow and "make ide" will fail. Use "make bin/coqide.byte"
 	instead. To fix this problem, just recompile OCaml from source
-	and configure with : "./configure --with-pthreads". 
+	and configure OCaml with : "./configure --with-pthreads". 
 	In case you install over an existing copy of OCaml, you
 	should better empty the OCaml installation directory.
 
@@ -64,8 +64,14 @@ INSTALLATION
 	make install-ide
 
 NOTES
-Font configuration is not saved.
-If you want to change the defaults fonts, just copy the
-.coqiderc file located in the ide subdir of the Coq library to
-your home directory and edit it by hand.
+There are two configuration files located in your $(HOME) dir. You may need to
+ set HOME to any sensible value under Windows.
+
+- .coqiderc is generated by coqide itself. It may be edited by hand or 
+  using the Preference menu from coqide. It will be generated the first time
+  you save your preferences in Coqide.
+
+- .coqide-gtk2rc is a standard Gtk2 configuration file. A sample file can be
+  found in the coq lib ide subdir.
+
 Read ide/FAQ for more informations.
diff --git a/Makefile b/Makefile
index 93654570d..dd5a8f874 100644
--- a/Makefile
+++ b/Makefile
@@ -399,7 +399,7 @@ beforedepend:: ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml
 beforedepend:: ide/config_parser.mli ide/config_parser.ml
 
 FULLIDELIB=$(FULLCOQLIB)/ide
-IDEFILES=ide/coq.png ide/.coqiderc
+IDEFILES=ide/coq.png ide/.coqide-gtk2rc
 
 ide: $(COQIDEBYTE) $(COQIDE) states
 clean-ide: 
diff --git a/ide/.coqiderc b/ide/.coqide-gtk2rc
index 49181175d..da2c5d929 100644
--- a/ide/.coqiderc
+++ b/ide/.coqide-gtk2rc
@@ -1,6 +1,13 @@
+# Some default functions for CoqIde. You may copy the file in your HOME and
+# edit as you want. See 
+# http://developer.gnome.org/doc/API/2.0/gtk/gtk-Resource-Files.html
+# for a complete set of options
+# To set the font of the text windows, edit the .coqiderc file through the menus.
+
+
 binding "text" {
   bind "<ctrl>k" { "set-anchor" ()
-		   "move-cursor" (display-lines,1,0)
+		   "move-cursor" (display-line-ends,1,0)
 		   "cut-clipboard" ()	
 		}
   bind "<ctrl>w" { "cut-clipboard" () }
@@ -13,7 +20,7 @@ class "GtkTextView" binding "text"
 
 
 style "views" {
-font_name = "Monospace 10"
+base[NORMAL] = "CornSilk"
 }
 class "GtkTextView" style "views"
 
@@ -21,16 +28,11 @@ widget "*.*.*.*.*.ScriptWindow" style "views"
 widget "*.*.*.*.GoalWindow" style "views"
 widget "*.*.*.*.MessageWindow" style "views"
 
-style "menu" {
-font_name = "Sans 12"
-}
-class "GtkLabel" style "menu"
-
+gtk-font-name = "Sans 12"
 
 style "location" {
 font_name = "Monospace 10"
 }
-widget "*.*.*.location" style "location"
-
+widget "*location*" style "location"
 
 gtk-key-theme-name = "Emacs"
diff --git a/ide/FAQ b/ide/FAQ
index e6e022973..e00131f7b 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -1,22 +1,13 @@
 Q1) How to enable Emacs keybindings?
 R1: Insert 
 	gtk-key-theme-name = "Emacs"
-    in your ".coqiderc" file. It may be in the current dir
-    or in $HOME dir.
+    in your ".coqide-gtk2rc" file. It may be in the current dir
+    or in $HOME dir. This is done by default.
 
-Q2) How to change the default font ?
-R2) Insert 
-	style "default" {
-	font_name = "Monospace 14"
-	}
-	class "GtkTextView" style "default"
-    in your .coqiderc file. See Q1.
-    You may replace Monospace 14 by anything reasonable describing 
-    a font. For example "Sans bold 22". See Pango Font Descriptions for more
-    informations (http://www.pango.org/).
 
-Q3) How to enable antialiased fonts?
-R3) Set the GDK_USE_XFT variable to 1.
+Q2) How to enable antialiased fonts?
+R2) Set the GDK_USE_XFT variable to 1. This is by default with Gtk >= 2.2.
+    If some of your fonts seem not to be available, set to 0.
 
 Q4) How can use Forall and Exists pretty symbols ?
 R4) Thanks to the Notation features in Coq, you just need to insert these
@@ -25,10 +16,14 @@ R4) Thanks to the Notation features in Coq, you just need to insert these
 Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10).
 Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
 ======================================================================
-Copy/Paste might not work. You need to load a file containing these lines or to enter 
-the "∀" using an input method. As a convenience, you may put these lines in
+Copy/Paste from this file will not work. 
+You need to load a file containing these lines or to enter the "∀" 
+using an input method. As a convenience, you may put these lines in
 a utf8.v file and start coqide with : 
 	coqide -l utf8.v
+In the ide subdir of Coq sources, you will find a sample utf8.v with some 
+notations
+
 
 
 Input Methods:
@@ -36,14 +31,14 @@ Input Methods:
 	2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀"	
 	in UTF-8.
 	2203 is for exists. See http://www.unicode.org for more.
--Second solution : rebind "<AltGr>a" to forall and "<AltGr>e" to exists. Under X11, you need to 
-	use something like
+-Second solution : rebind "<AltGr>a" to forall and "<AltGr>e" to exists. 
+	Under X11, you need to use something like
 		xmodmap -e "keycode  24 = a A F13 F13" 
 		xmodmap -e "keycode  26 = e E F14 F14" 
 	and then to add   
 		bind "F13" {"insert-at-cursor" ("∀")}
 		bind "F14" {"insert-at-cursor" ("∃")}
-	to your "binding "text"" section in .coqiderc. 
+	to your "binding "text"" section in .coqiderc-gtk2rc.
 	The strange ("∀") argument is the UTF-8 encoding for
 	0x2200. It is computed by lablgtk2 by 
 		Glib.Utf8.from_unichar 0x2200;;
diff --git a/ide/coqide.ml b/ide/coqide.ml
index d8a44278d..11269de89 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -22,11 +22,6 @@ let window_height = 600
 
 let initial_cwd = Sys.getcwd ()
 
-let default_general_font_name = "Sans 14"
-let default_monospace_font_name = "Monospace 14"
-
-let manual_monospace_font = ref None
-let manual_general_font = ref None
 
 let status = ref None
 let push_info = ref (function s -> failwith "not ready")
@@ -37,17 +32,6 @@ let set_location = ref  (function s -> failwith "not ready")
 
 let pulse = ref (function () -> failwith "not ready")
 
-let has_config_file = 
-  (Sys.file_exists (Filename.concat lib_ide ".coqiderc")) || 
-  (try Sys.file_exists (Filename.concat (Sys.getenv "HOME") ".coqiderc")
-   with Not_found -> false)
-
-let () = if not has_config_file then 
-  manual_monospace_font := Some 
-    (Pango.Font.from_string default_monospace_font_name);
-  manual_general_font := Some 
-    (Pango.Font.from_string default_general_font_name)
-
 let (font_selector:GWindow.font_selection_dialog option ref) = ref None
 let (message_view:GText.view option ref) = ref None
 let (proof_view:GText.view option ref) = ref None
@@ -196,8 +180,8 @@ let (input_views:analyzed_views viewable_script Vector.t) = Vector.create ()
 
 let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; 
 			  Sys.sigill; Sys.sigpipe; Sys.sigquit; 
-			  (* Sys.sigsegv;*)  Sys.sigterm; Sys.sigusr2] 
-			
+			  (* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2] 
+
 let crash_save i =
 (*  ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
   Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files";
@@ -219,7 +203,7 @@ let crash_save i =
     )
     input_views;
   Pervasives.prerr_endline "Done. Please report.";
-  exit i
+  if i <> 127 then exit i
 
 let ignore_break () = 
   List.iter 
@@ -1463,9 +1447,7 @@ let main files =
       with_file f ~f:(input_channel b);
       let s = do_convert (Buffer.contents b) in
       let view = create_input_tab (Glib.Convert.filename_to_utf8 (Filename.basename f)) in
-      (match !manual_monospace_font with
-	 | None -> ()
-	 | Some n -> view#misc#modify_font n);
+      view#misc#modify_font !current.text_font;
       let index = add_input_view {view = view;
 				  analyzed_view = None;
 				 }
@@ -1677,10 +1659,10 @@ let main files =
 	       (get_current_view()).view#buffer;
 	       (out_some (get_current_view()).analyzed_view)#recenter_insert));
 
-  (* File/Refresh Menu *)
+(*  (* File/Refresh Menu *)
   let refresh_m = file_factory#add_item "Restart all" ~key:GdkKeysyms._R in
   refresh_m#misc#set_state `INSENSITIVE;
-
+*)
   (* File/Quit Menu *)
   let quit_f () =
     if has_something_to_save () then 
@@ -1718,7 +1700,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 
@@ -1731,7 +1713,7 @@ let main files =
 		   GtkText.View.Signals.paste_clipboard
 		 with _ -> prerr_endline "EMIT PASTE FAILED")));
   ignore (edit_f#add_separator ());
-  let read_only_i = edit_f#add_check_item "Read only" ~active:false
+  let read_only_i = edit_f#add_check_item "_Read only" ~active:false
 		      ~callback:(fun b -> 
 				   let v = get_current_view () in
 				   v.view#set_editable (not b);
@@ -1739,14 +1721,13 @@ let main files =
 				) 
   in
   read_only_i#misc#set_state `INSENSITIVE;
-  let search_i = edit_f#add_item "Search"
+  let search_if = edit_f#add_item "Search _forward"
 		   ~key:GdkKeysyms._F
-		   ~callback:(fun b -> 
-				let v = get_current_view () in 
-				!flash_info "Search Unsupported"
-			     ) 
   in
-  let complete_i = edit_f#add_item "Complete"
+  let search_ib = edit_f#add_item "Search _backward"
+		   ~key:GdkKeysyms._R
+  in
+  let complete_i = edit_f#add_item "_Complete"
 		     ~key:GdkKeysyms._comma
 		     ~callback:
 		     (do_if_not_computing 
@@ -2042,22 +2023,18 @@ let main files =
     configuration_factory#add_item "Edit _preferences"
       ~callback:(fun () -> configure ();reset_revert_timer ())
   in
-  (* let save_prefs_m =
-     configuration_factory#add_item "Save preferences"
-     ~callback:(fun () ->
-     let fd = open_out "toto" in
-     output_pref fd current;
-     close_out fd)
-     in
-  *)
+  let save_prefs_m =
+    configuration_factory#add_item "_Save preferences"
+      ~callback:(fun () -> save_pref !current)
+  in
   font_selector := 
   Some (GWindow.font_selection_dialog 
 	  ~title:"Select font..."
 	  ~modal:true ());
   let font_selector = out_some !font_selector in
-  font_selector#selection#set_font_name default_monospace_font_name;
-  font_selector#selection#set_preview_text 
-    "Lemma Truth: (p:Prover) `p < Coq`. Proof. Auto with *. Save."; 
+  font_selector#selection#set_font_name (Pango.Font.to_string !current.text_font);
+  font_selector#selection#set_preview_text
+    "Lemma Truth: ∀ p:Prover, `p < Coq`. Proof. Auto with *. Save."; 
   let customize_fonts_m = 
     configuration_factory#add_item "Customize _fonts"
       ~callback:(fun () -> font_selector#present ())
@@ -2120,6 +2097,100 @@ let main files =
   let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
   let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) () 
   in
+  let search_lbl = GMisc.label ~text:"Search:"
+		 ~show:true
+		 ~packing:(lower_hbox#pack ~expand:false) () 
+  in
+  let search_history = ref [] in
+  let search_input = GEdit.combo ~popdown_strings:!search_history
+		       ~use_arrows:`DEFAULT
+		       ~show:true
+		       ~packing:(lower_hbox#pack ~expand:false) () 
+  in
+  search_input#disable_activate ();
+  let ready_to_wrap_search = ref false in
+  let start_of_search = ref None in
+  let search_forward = ref true in
+  ignore (search_input#entry#connect#activate 
+	    ~callback:
+	    (fun () -> 
+	       if not (List.mem search_input#entry#text !search_history) then
+	       (search_history := 
+	       search_input#entry#text::!search_history;
+	       search_input#set_popdown_strings !search_history);
+	       let v = (get_current_view ()).view in
+	       v#coerce#misc#grab_focus ();
+	       v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT);
+	       search_input#entry#set_text ""; 
+	       start_of_search := None;
+	       ready_to_wrap_search := false
+	    )) ;
+
+  to_do_on_page_switch := 
+  (fun i -> 
+     start_of_search := None;
+     ready_to_wrap_search:=false)::!to_do_on_page_switch;
+  let rec search_f () = 
+    if !start_of_search = None then 
+      start_of_search := 
+      Some ((get_current_view ()).view#buffer#create_mark 
+	      ((get_current_view ()).view#buffer#get_iter_at_mark `INSERT));
+    let txt = search_input#entry#text in 
+	       let v = (get_current_view ()).view in 
+	       let iit = v#buffer#get_iter_at_mark `SEL_BOUND in
+	       (match 
+		  if !search_forward then iit#forward_search txt 
+		  else (find_word_end iit)#backward_search txt 
+		with 
+		 | None -> 
+		     if !ready_to_wrap_search then begin
+		       ready_to_wrap_search := false;
+		       !flash_info "Search wrapped";
+		       v#buffer#place_cursor 
+			 (if !search_forward then v#buffer#start_iter else
+			 v#buffer#end_iter);
+		       search_f ()
+		     end else begin
+		       if !search_forward then !flash_info "Search at end"
+		       else !flash_info "Search at start";
+		       ready_to_wrap_search := true
+		     end
+		 | Some (start,stop) -> 
+		     v#buffer#move_mark `SEL_BOUND start;
+		     v#buffer#move_mark `INSERT stop;
+		     v#scroll_to_mark `INSERT
+	       ) 
+  in  
+  ignore (search_input#entry#event#connect#key_release 
+	    ~callback:
+	    (fun ev ->
+	       if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin
+		       let v = (get_current_view ()).view in
+		       (match !start_of_search with 
+			 | None -> 
+			     v#buffer#move_mark 
+			     `SEL_BOUND 
+			     (v#buffer#get_iter_at_mark `INSERT)
+			 | Some mk -> let it = v#buffer#get_iter_at_mark 
+						 (`MARK mk) in
+			   v#buffer#place_cursor it;
+			   start_of_search := None
+		       );
+		       search_input#entry#set_text ""; 
+		       v#coerce#misc#grab_focus ();
+	       end else search_f (); 
+	       false
+	    )) ;
+  ignore (search_if#connect#activate
+    ~callback:(fun b -> 
+		 search_forward:= true;
+		 search_input#entry#coerce#misc#grab_focus (); 
+	      ));
+  ignore (search_ib#connect#activate
+    ~callback:(fun b ->
+		 search_forward:= false;
+		 search_input#entry#coerce#misc#grab_focus (); 
+	      ));
   let status_context = status_bar#new_context "Messages" in
   let flash_context = status_bar#new_context "Flash" in
   ignore (status_context#push "Ready");
@@ -2129,7 +2200,7 @@ let main files =
   flash_info := (fun s -> flash_context#flash ~delay:5000 s);
 
   (* Location display *)
-  let l = GMisc.label 
+  let l = GMisc.label
 	     ~text:"Line:     1 Char:   1" 
 	     ~packing:lower_hbox#pack () in 
   l#coerce#misc#set_name "location";
@@ -2190,7 +2261,7 @@ let main files =
 				Vector.iter 
 				  (fun {view=view} -> view#misc#modify_font pango_font)
 				  input_views;
-				manual_monospace_font := Some pango_font
+				!current.text_font <- pango_font
 			 );
 			 font_selector#misc#hide ()));
 
@@ -2228,12 +2299,9 @@ let main files =
   (get_input_view index).analyzed_view <- Some (new analyzed_view index);
   activate_input index;
   set_tab_image index yes_icon;
-  (match !manual_monospace_font with 
-     | None -> ()
-     | Some f -> 
-	 view#misc#modify_font f; 
-	 tv2#misc#modify_font f; 
-	 tv3#misc#modify_font f);
+  view#misc#modify_font !current.text_font; 
+  tv2#misc#modify_font !current.text_font; 
+  tv3#misc#modify_font !current.text_font;
   ignore (about_m#connect#activate 
 	    ~callback:(fun () -> tv3#buffer#set_text "by Benjamin Monate"));
   ignore (w#misc#connect#size_allocate 
@@ -2267,9 +2335,9 @@ let main files =
 let start () = 
   let files = Coq.init () in
   ignore_break ();
-  GtkMain.Rc.add_default_file (Filename.concat lib_ide ".coqiderc");
+  GtkMain.Rc.add_default_file (Filename.concat lib_ide ".coqide-gtk2rc");
   (try 
-     GtkMain.Rc.add_default_file (Filename.concat (Sys.getenv "HOME") ".coqiderc");
+     GtkMain.Rc.add_default_file (Filename.concat (Sys.getenv "HOME") ".coqide-gtk2rc");
   with Not_found -> ());
   ignore (GtkMain.Main.init ());
   GtkData.AccelGroup.set_default_mod_mask 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 4370ca985..10071161b 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -3,8 +3,8 @@ open Printf
 open Util
 
 let pref_file = 
-  try (Filename.concat (Sys.getenv "HOME") ".coqidepref")
-  with _ -> ".coqidepref"
+  try (Filename.concat (Sys.getenv "HOME") ".coqiderc")
+  with _ -> ".coqiderc"
 
 let mod_to_str (m:Gdk.Tags.modifier) = 
   match m with
@@ -63,6 +63,8 @@ type pref =
 
       mutable cmd_browse : string * string;
 
+      mutable text_font : Pango.font_description;
+
       mutable doc_url : string;
       mutable library_url : string;
     }
@@ -94,6 +96,9 @@ let save_pref p =
     add "modifiers_valid" 
       (List.map mod_to_str p.modifiers_valid) ++
     add "cmd_browse" [fst p.cmd_browse; snd p.cmd_browse] ++
+
+    add "text_font" [Pango.Font.to_string p.text_font] ++
+
     add "doc_url" [p.doc_url] ++
     add "library_url" [p.library_url] ++
     Config_lexer.print_file pref_file
@@ -130,6 +135,8 @@ let (current:pref ref) =
 
     
     cmd_browse = "netscape -remote \"OpenURL(", ")\"";
+    
+    text_font = Pango.Font.from_string "Monospace 12";
 
     doc_url = "http://coq.inria.fr/doc/";
     library_url = "http://coq.inria.fr/library/";
@@ -171,10 +178,13 @@ let load_pref p =
     set "modifiers_valid" 
       (fun v -> np.modifiers_valid <- List.map str_to_mod v);
     set_pair "cmd_browse" (fun v1 v2 -> np.cmd_browse <- (v1,v2));
+    set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v);
     set_hd "doc_url" (fun v -> np.doc_url <- v);
     set_hd "library_url" (fun v -> np.library_url <- v);
     current := np
-  with e -> prerr_endline (Printexc.to_string e); prerr_endline "Could not load preferences."
+  with e -> 
+    prerr_endline ("Could not load preferences ("^
+		   (Printexc.to_string e)^").")
 
 let configure () = 
   let cmd_coqc =