search window

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

6 files changed, 59 insertions, 37 deletions

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 86b7744c9..640d1c383 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -120,6 +120,7 @@ let commands = [
    "Remove Printing Let";
    "Require";
    "Require Export";
+   "Require Import";
    (* "Reset"; *)
    "Reset Extraction Inline";
    (* "Reset Initial"; *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0eb05dd99..02025bfbb 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1720,6 +1720,11 @@ let main files =
 	    ~width:!current.window_width ~height:!current.window_height 
 	    ~title:"CoqIde" ()
   in
+(*
+  let icon_image = Filename.concat lib_ide "coq.ico" in
+  let icon = GdkPixbuf.from_file icon_image in
+  w#set_icon (Some icon);
+*)
   let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
 
 
@@ -2077,7 +2082,7 @@ let main files =
 		 ~title:"CoqIde search/replace" ()
   in
   let find_box = GPack.table
-		   ~columns:3 ~rows:3
+		   ~columns:3 ~rows:5
 		   ~col_spacings:10 ~row_spacings:10 ~border_width:10
 		   ~homogeneous:false ~packing:find_w#add () in
   
@@ -2135,6 +2140,18 @@ let main files =
       ~packing: (find_box#attach ~left:2 ~top:2)
       ()
   in
+  let find_again_button =
+    GButton.button
+      ~label:"_Find again"
+      ~packing: (find_box#attach ~left:2 ~top:3)
+      ()
+  in
+  let find_again_backward_button =
+    GButton.button
+      ~label:"Find _backward"
+      ~packing: (find_box#attach ~left:2 ~top:4)
+      ()
+  in
   let last_find () =
     let v = (get_current_view()).view in
     let b = v#buffer in
@@ -2194,6 +2211,18 @@ let main files =
     find_w#misc#hide();
     v#coerce#misc#grab_focus()
   in
+  let find_again_forward () =
+    search_backward := false;
+    let (v,b,start,_) = last_find () in
+    let start = start#forward_chars 1 in
+    find_from v b start find_entry#text
+  in
+  let find_again_backward () =
+    search_backward := true;
+    let (v,b,start,_) = last_find () in
+    let start = start#backward_chars 1 in
+    find_from v b start find_entry#text
+  in
   let key_find ev =
     let s = GdkEvent.Key.state ev and k = GdkEvent.Key.keyval ev in
     if k = GdkKeysyms._Escape then
@@ -2210,28 +2239,16 @@ let main files =
       end 
     else if List.mem `CONTROL s && k = GdkKeysyms._f then
       begin
-	search_backward := false;
-	let (v,b,start,_) = last_find () in
-	let start = start#forward_chars 1 in
-	find_from v b start find_entry#text;
+	find_again_forward ();
 	true
       end
     else if List.mem `CONTROL s && k = GdkKeysyms._b then
       begin
-	search_backward := true;
-	let (v,b,start,_) = last_find () in
-	let start = start#backward_chars 1 in
-	find_from v b start find_entry#text;
+	find_again_backward ();
 	true
       end
     else false (* to let default callback execute *)
   in
-  let _ = close_find_button#connect#clicked close_find in
-  let _ = replace_button#connect#clicked do_replace in
-  let _ = replace_find_button#connect#clicked do_replace_find in
-  let _ = find_entry#connect#changed do_find in
-  let _ = find_entry#event#connect#key_press ~callback:key_find in
-  let _ = find_w#event#connect#delete (fun _ -> find_w#misc#hide(); true) in
   let find_f ~backward () = 
     search_backward := backward;
     find_w#show ();
@@ -2242,10 +2259,18 @@ let main files =
 		 ~key:GdkKeysyms._F
 		 ~callback:(find_f ~backward:false)
   in
-  let find_back_i = edit_f#add_item "_Find backwards"
+  let find_back_i = edit_f#add_item "Find _backwards"
 		 ~key:GdkKeysyms._B
 		 ~callback:(find_f ~backward:true)
   in
+  let _ = close_find_button#connect#clicked close_find in
+  let _ = replace_button#connect#clicked do_replace in
+  let _ = replace_find_button#connect#clicked do_replace_find in
+  let _ = find_again_button#connect#clicked find_again_forward in
+  let _ = find_again_backward_button#connect#clicked find_again_backward in
+  let _ = find_entry#connect#changed do_find in
+  let _ = find_entry#event#connect#key_press ~callback:key_find in
+  let _ = find_w#event#connect#delete (fun _ -> find_w#misc#hide(); true) in
 (*
   let search_if = edit_f#add_item "Search _forward"
 		    ~key:GdkKeysyms._greater
@@ -2280,7 +2305,7 @@ let main files =
   ignore(edit_f#add_separator ());
   (* external editor *)
   let _ = 
-    edit_f#add_item "External editor" ~key:GdkKeysyms._E ~callback:
+    edit_f#add_item "External editor" ~callback:
       (fun () -> 	 
 	 let av = out_some ((get_current_view()).analyzed_view) in 
 	 match av#filename with
@@ -3296,7 +3321,7 @@ let start () =
   ignore_break ();
   GtkMain.Rc.add_default_file (Filename.concat lib_ide ".coqide-gtk2rc");
   (try 
-     GtkMain.Rc.add_default_file (Filename.concat (Sys.getenv "HOME") ".coqide-gtk2rc");
+     GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
   with Not_found -> ());
   ignore (GtkMain.Main.init ());
   GtkData.AccelGroup.set_default_mod_mask 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 19f5070b4..925199ecd 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -210,10 +210,10 @@ let find_tag_stop (tag :GText.tag) (it:GText.iter) =
 let find_tag_limits (tag :GText.tag) (it:GText.iter) = 
  (find_tag_start tag it , find_tag_stop tag it)
 
-let async =
-(* 
-  if Sys.os_type <> "Unix" then GtkThread.async else (fun x -> x)
-*) fun x -> x
+(* explanations ?? *)
+let async = 
+  if Sys.os_type <> "Unix" then GtkThread.async else 
+    (fun x -> x)
 
 let stock_to_widget ?(size=`DIALOG) s = 
   let img = GMisc.image () 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 309cc150e..c4976748e 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -12,13 +12,9 @@ open Configwin
 open Printf
 open Util
 
-let pref_file = 
-  try (Filename.concat (Sys.getenv "HOME") ".coqiderc")
-  with _ -> ".coqiderc"
+let pref_file = Filename.concat System.home ".coqiderc"
 
-let accel_file = 
-  try (Filename.concat (Sys.getenv "HOME") ".coqide.keys")
-  with _ -> ".coqide.keys"
+let accel_file = Filename.concat System.home ".coqide.keys"
 
 let mod_to_str (m:Gdk.Tags.modifier) = 
   match m with
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 97ab8a9b7..719f7434a 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -33,15 +33,15 @@ let report () = (str "." ++ spc () ++ str "Please report.")
 
 let rec explain_exn_default = function
   | Stream.Failure -> 
-      hov 0 (str "Anomaly: Uncaught Stream.Failure.")
+      hov 0 (str "Anomaly: uncaught Stream.Failure.")
   | Stream.Error txt -> 
       hov 0 (str "Syntax error: " ++ str txt)
   | Token.Error txt -> 
       hov 0 (str "Syntax error: " ++ str txt)
   | Sys_error msg -> 
-      hov 0 (str "Error: OS: " ++ str msg)
+      hov 0 (str "Anomaly: uncaught exception Sys_error " ++ str (guill msg) ++ report ())
   | UserError(s,pps) -> 
-      hov 1 (str"Error: " ++ where s ++ pps)
+      hov 1 (str "User error: " ++ where s ++ pps)
   | Out_of_memory -> 
       hov 0 (str "Out of memory")
   | Stack_overflow -> 
@@ -56,13 +56,13 @@ let rec explain_exn_default = function
 	       int pos1 ++ str " to #" ++ int pos2 ++
 	       report ())
   | Not_found -> 
-      hov 0 (str "Anomaly: Search error" ++ report ())
+      hov 0 (str "Anomaly: uncaught exception Not_found" ++ report ())
   | Failure s -> 
-      hov 0 (str "Anomaly: Failure " ++ str (guill s) ++ report ())
+      hov 0 (str "Anomaly: uncaught exception Failure " ++ str (guill s) ++ report ())
   | Invalid_argument s -> 
-      hov 0 (str "Anomaly: Invalid argument " ++ str (guill s) ++ report ())
+      hov 0 (str "Anomaly: uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
   | Sys.Break -> 
-      hov 0 (fnl () ++ str"User Interrupt.")
+      hov 0 (fnl () ++ str "User Interrupt.")
   | Univ.UniverseInconsistency -> 
       hov 0 (str "Error: Universe Inconsistency.")
   | TypeError(ctx,te) -> 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6c82aaad0..7c1995454 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -620,13 +620,13 @@ let vernac_add_ml_path isrec s =
 let vernac_declare_ml_module l = Mltop.declare_ml_modules l
 
 let vernac_chdir = function
-  | None -> print_endline (Sys.getcwd())
+  | None -> message (Sys.getcwd())
   | Some s ->
       begin
 	try Sys.chdir (System.glob s)
 	with Sys_error str -> warning ("Cd failed: " ^ str)
       end;
-      if_verbose print_endline (Sys.getcwd())
+      if_verbose message (Sys.getcwd())
 
 
 (********************)