ameliorations coqide

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

11 files changed, 738 insertions, 277 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 0d1b9fa75..0e2d5a378 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -8,40 +8,15 @@
 
 (* $Id$ *)
 
-let decompose_tab w = 
-  let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in
-  let l = vbox#children in
-  match l with 
-    | [img;lbl] -> 
-	let img = new GMisc.image 
-		    ((Gobject.try_cast img#as_widget "GtkImage"):
-		       Gtk.image Gtk.obj) 
-	in
-	let lbl = GMisc.label_cast lbl in
-	vbox,img,lbl
-    | _ -> assert false
-
-
 class command_window () = 
   let window = GWindow.window 
 		 ~allow_grow:true ~allow_shrink:true 
 		 ~width:320 ~height:200
+		 ~position:`CENTER
 		 ~title:"CoqIde queries" ~show:false ()
   in
   let accel_group = GtkData.AccelGroup.create () in
   let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in
-(*
-  let menubar = GMenu.menu_bar ~packing:vbox#pack () in
-*)
-(*
-  let handle = GBin.handle_box 
-		 ~show:true
-		 ~handle_position:`LEFT
-		 ~snap_edge:`LEFT
-		 ~packing:vbox#pack
-		 ()
-  in
-*)
   let toolbar = GButton.toolbar 
 		  ~orientation:`HORIZONTAL 
 		  ~style:`ICONS
@@ -51,13 +26,6 @@ class command_window () =
 			       ~fill:false)
 		  ()
   in
-(*
-  let factory = new GMenu.factory menubar
-  in
-*)
-(*
-  let accel_group = factory#accel_group in
-*)
   let notebook = GPack.notebook ~scrollable:true 
 		   ~packing:(vbox#pack 
 			       ~expand:true
@@ -65,10 +33,6 @@ class command_window () =
 			    ) 
 		   ()
   in
-(*
-  let hide_menu = factory#add_item "_Hide Window" 
-		    ~callback:window#misc#hide
-*)
   let _ = 
     toolbar#insert_button
       ~tooltip:"Hide Window"
@@ -77,9 +41,6 @@ class command_window () =
       ~callback:window#misc#hide
       ()
   in
-(*
-  let new_page_menu = factory#add_item "_New Page" in
-*)
   let new_page_menu = 
     toolbar#insert_button
       ~tooltip:"New Page"
@@ -91,13 +52,6 @@ class command_window () =
       ()
   in
 
-(*
-  let kill_page_menu = 
-    factory#add_item "_Kill Page" 
-      ~callback:
-      (fun () -> notebook#remove_page notebook#current_page)
-  in
-*)
   let kill_page_menu = 
     toolbar#insert_button
       ~tooltip:"Kill Page"
diff --git a/ide/coq.ml b/ide/coq.ml
index cf54bfa2a..f8467f4f2 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -134,7 +134,8 @@ let interp s =
 		  | VernacCheckMayEval _
 		  | VernacGlobalCheck _
 		  | VernacPrint _
-		  | VernacSearch _ ->   ()
+		  | VernacSearch _ ->   
+		      !flash_info ~delay:1000000 "Warning: query commands should not be inserted in scripts" 
 		  | _ -> ()
 	      end;
 	      Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 7173bfc2f..86b7744c9 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -38,9 +38,9 @@ let commands = [
    "Defined.";
    "Definition";
    "Derive Dependent Inversion";
-   "Derive Dependent Inversion_clear";
+   "Derive Dependent Inversion__clear";
    "Derive Inversion";
-   "Derive Inversion_clear";
+   "Derive Inversion__clear";
    (* "Drop"; *)];
   ["End";
    "End Silent.";
@@ -141,7 +141,7 @@ let commands = [
      "Section";
      "Set Extraction AutoInline";
      "Set Extraction Optimize";
-     "Set Hyps_limit";
+     "Set Hyps__limit";
      "Set Implicit Arguments";
      "Set Printing Coercion";
      "Set Printing Coercions";
@@ -174,7 +174,7 @@ let commands = [
    "Unfocus";
    "Unset Extraction AutoInline";
    "Unset Extraction Optimize";
-   "Unset Hyps_limit";
+   "Unset Hyps__limit";
    "Unset Implicit Arguments";
    "Unset Printing Coercion";
    "Unset Printing Coercions";
@@ -240,3 +240,192 @@ let state_preserving = [
   "Test Printing Synth";
   "Test Printing Wildcard";
 ]
+
+
+let tactics = 
+  [
+    [
+      "abstract";
+      "absurd";
+      "apply";
+      "apply __ with";
+      "assert";
+      "assumption.";
+      "auto.";
+      "auto with";
+      "autorewrite";
+    ];
+
+   [
+     "case";
+     "case __ with";
+     "cbv";
+     "change";
+     "change __ in";
+     "clear";
+     "clearbody";
+     "compare";
+     "compute";
+     "congruence";
+     "constructor";
+     "constructor __ with";
+     "contradiction.";
+     "cut";
+     "cutrewrite";
+   ];
+
+   [
+     "decide equality.";
+     "decompose";
+     "decompose record";
+     "decompose sum";
+     "dependent inversion";
+     "dependent inversion __ with";
+     "dependent inversion__clear";
+     "dependent inversion__clear __ with";
+     "dependent rewrite ->";
+     "dependent rewrite <-";
+     "destruct";
+     "discriminate.";
+     "discriminate";
+     "discrR.";
+     "do";
+     "double induction";
+   ];
+
+   [
+     "eapply";
+     "eauto.";
+     "eauto with";
+     "elim";
+     "elim __ using";
+     "elim __ with";
+     "elimtype";
+     "exact";
+     "exists";
+   ];
+
+   [
+     "fail.";
+     "field.";
+     "first";
+     "firstorder.";
+     "firstorder";
+     "firstorder using";
+     "firstorder with";
+     "fold";
+     "fourier.";
+     "functional induction";
+   ];
+
+   [
+     "generalize";
+     "generalize dependent";
+   ];
+   
+   [
+     "hnf";
+   ];
+
+   [
+     "idtac.";
+     "induction";
+     "info";
+     "injection";
+     "intro";
+     "intro after";
+     "intro __ after";
+     "intros";
+     "intros.";
+     "intros";
+     "intros <pattern> ";
+     "intros until";
+     "intuition.";
+     "intuition";
+     "inversion";
+     "inversion __ in";
+     "inversion __ using";
+     "inversion __ using __ in";
+     "inversion__clear";
+     "inversion__clear __ in";
+   ];
+
+   [
+     "jp <n>";
+     "jp.";
+   ];
+
+   [
+     "lapply";
+     "lazy";
+     "left";
+   ];
+
+   [
+     "move __ after";
+   ];
+
+   [
+     "omega";
+   ];
+
+   [
+     "pattern";
+     "pose";
+     "progress";
+   ];
+
+   [
+     "quote";
+   ];
+
+   [
+     "red.";
+     "red in";
+     "refine";
+     "reflexivity.";
+     "rename __ into";
+     "repeat";
+     "replace __ with";
+     "rewrite";
+     "rewrite __ in";
+     "rewrite ->";
+     "rewrite -> __ in";
+     "rewrite <-";
+     "rewrite <- __ in";
+     "right.";
+     "ring.";
+   ];
+
+   [
+     "set";
+     "setoid__replace";
+     "setoid__rewrite";
+     "simpl.";
+     "simpl __ in";
+     "simple destruct";
+     "simple induction";
+     "simple inversion";
+     "simplify__eq";
+     "solve";
+     "split.";
+     "split__Rabs.";
+     "split__Rmult.";
+     "subst";
+     "symmetry.";
+   ];
+
+   [
+     "tauto.";
+     "transitivity";
+     "trivial.";
+     "try";
+   ];
+   
+   [
+     "unfold";
+     "unfold __ in";
+   ];
+]
+
+
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 201f44c93..0eb05dd99 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -12,7 +12,6 @@ open Preferences
 open Vernacexpr
 open Coq
 open Ideutils
-open Format
 
 let out_some s = match s with 
   | None -> failwith "Internal error in out_some" | Some f -> f
@@ -21,16 +20,6 @@ let cb_ = ref None
 let cb () = ((out_some !cb_):GData.clipboard)
 let last_cb_content = ref ""
 
-let yes_icon = `YES
-let no_icon = `NO
-let save_icon = `SAVE
-let saveas_icon = `SAVE_AS
-let warning_icon = `DIALOG_WARNING
-let dialog_size = `DIALOG
-let small_size = `SMALL_TOOLBAR
-
-let initial_cwd = Sys.getcwd ()
-
 let (message_view:GText.view option ref) = ref None
 let (proof_view:GText.view option ref) = ref None
 
@@ -61,14 +50,14 @@ let set_tab_label i n =
   (* lbl#set_text n *) lbl#set_label n
 
 
-let set_tab_image i s = 
+let set_tab_image ~icon i = 
   let nb = notebook () in
   let _,img,_ = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
   in
-  img#set_icon_size small_size;
-  img#set_stock s
+  img#set_icon_size `SMALL_TOOLBAR;
+  img#set_stock icon
 
-let set_current_tab_image s = set_tab_image (notebook())#current_page s
+let set_current_tab_image ~icon = set_tab_image ~icon (notebook())#current_page
   
 let set_current_tab_label n = set_tab_label (notebook())#current_page n 
 
@@ -100,6 +89,7 @@ module Vector = struct
   exception Found of int
   type 'a t = ('a option) array ref
   let create () = ref [||]
+  let length t = Array.length !t
   let get t i = out_some (Array.get !t i)
   let set t i v = Array.set !t i (Some v)
   let remove t i = Array.set !t i None
@@ -164,9 +154,6 @@ object('self)
     method active_keypress_handler : GdkEvent.Key.t -> bool
     method backtrack_to : GText.iter -> unit
     method backtrack_to_no_lock : GText.iter -> unit
-(*
-    method backtrack_to_insert : unit
-*)
     method clear_message : unit
     method deactivate : unit -> unit
     method disconnected_keypress_handler : GdkEvent.Key.t -> bool
@@ -178,17 +165,11 @@ object('self)
     method go_to_insert : unit
     method indent_current_line : unit
     method insert_command : string -> string -> unit
-(*
-    method insert_commands : (string * string) list -> unit
-*)
     method tactic_wizard : string list -> unit
     method insert_message : string -> unit
     method insert_this_phrase_on_success :
       bool -> bool -> bool -> string -> string -> bool
     method process_next_phrase : bool -> bool -> bool
-(*
-    method process_until_insert_or_error : unit
-*)
     method process_until_iter_or_error : GText.iter -> unit
     method process_until_end_or_error : unit
     method recenter_insert : unit
@@ -264,11 +245,11 @@ let break () =
     prerr_endline "Break received and discarded (not computing)"
   end
 
-let full_do_if_not_computing f x = 
+let full_do_if_not_computing text f x = 
     ignore (Thread.create 
 	      (async (fun () ->
 			if Mutex.try_lock coq_computing then begin
-			  prerr_endline "Launching thread";
+			  prerr_endline ("Launching thread " ^ text);
 			  let w = Blaster_window.blaster_window () in
 			  if not (Mutex.try_lock w#lock) then begin 
 			    break ();
@@ -300,14 +281,18 @@ let full_do_if_not_computing f x =
 			    "Discarded order (computations are ongoing)"))
 	      ())
 
-let do_if_not_computing f x = 
-  ignore (full_do_if_not_computing f x)
+let do_if_not_computing text f x = 
+  ignore (full_do_if_not_computing text f x)
 
 
 let add_input_view tv = 
   Vector.append input_views tv
 
-let get_input_view i = Vector.get input_views i
+let get_input_view i = 
+  if 0 <= i && i < Vector.length input_views
+  then
+    Vector.get input_views i
+  else raise Not_found 
 
 let active_view = ref None
 
@@ -658,7 +643,7 @@ object(self)
 			     "Overwrite File";
 			     "Disable Auto Revert"] 
 		   ~default:0
-		   ~icon:(stock_to_widget warning_icon)
+		   ~icon:(stock_to_widget `DIALOG_WARNING)
 		   "Some unsaved buffers changed on disk"
 		)
 	  with 1 -> do_revert ()
@@ -721,8 +706,8 @@ object(self)
 	       ~default:1
 	       ~icon:
 	       (let img = GMisc.image () in
-		img#set_stock warning_icon;
-		img#set_icon_size dialog_size;
+		img#set_stock `DIALOG_WARNING;
+		img#set_icon_size `DIALOG;
 		img#coerce)
 	       ("File "^f^"already exists")
 	    )
@@ -1190,12 +1175,6 @@ object(self)
   method process_until_end_or_error = 
     self#process_until_iter_or_error input_buffer#end_iter
 
-(*
-  method process_until_insert_or_error = 
-    let stop = self#get_insert in
-    self#process_until_iter_or_error stop
-*)
-
   method reset_initial =
     Stack.iter 
       (function inf -> 
@@ -1283,11 +1262,6 @@ Please restart and report NOW.";
        !pop_info ())
     else prerr_endline "backtrack_to : discarded (lock is busy)"
 
-(*
-  method backtrack_to_insert = 
-    self#backtrack_to self#get_insert
-*)
-
   method go_to_insert =
     let point = self#get_insert in
     if point#compare self#get_start_of_input>=0
@@ -1410,14 +1384,6 @@ Please restart and report NOW.";
   method insert_command cp ip = 
     self#clear_message;
     ignore (self#insert_this_phrase_on_success true false false cp ip)
-(*
-  method insert_commands l = 
-    self#clear_message;
-    ignore (List.exists 
-	      (fun (cp,ip) -> 
-		 self#insert_this_phrase_on_success true false false 
-		 (cp^"\n") (ip^"\n")) l)
-*)
 
   method tactic_wizard l =
     self#clear_message;
@@ -1558,7 +1524,9 @@ Please restart and report NOW.";
 		   | _ -> ())
 	   )
 
-  method help_for_keyword () = browse_keyword (get_current_word ())
+  method help_for_keyword () = 
+    
+    browse_keyword (self#insert_message) (get_current_word ())
 
   initializer 
     ignore (message_buffer#connect#insert_text
@@ -1605,11 +1573,11 @@ Please restart and report NOW.";
 	 (fun () ->
 	    if input_buffer#modified then 
 	      set_tab_image index 
-		(match (out_some (current_all.analyzed_view))#filename with 
-		 | None -> saveas_icon
-		 | Some _ -> save_icon
+		~icon:(match (out_some (current_all.analyzed_view))#filename with 
+		 | None -> `SAVE_AS
+		 | Some _ -> `SAVE
 		)
-	    else set_tab_image index yes_icon;
+	    else set_tab_image index ~icon:`YES;
 	 ));
     ignore (input_buffer#connect#changed
 	      ~callback:(fun () -> 
@@ -1716,11 +1684,31 @@ let create_input_tab filename =
   ignore (tv1#buffer#create_tag 
 	    ~name:"processed" 
 	    [`BACKGROUND "light green" ;`EDITABLE false]);
+  ignore (tv1#buffer#create_tag 
+	    ~name:"found" 
+	    [`BACKGROUND "blue"; `FOREGROUND "white"]);
   tv1
 
 
 let last_make = ref "";;
- 
+let last_make_index = ref 0;;
+let search_compile_error_regexp =
+  Str.regexp
+    "File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)";;
+
+let search_next_error () =
+  let _ = Str.search_forward search_compile_error_regexp !last_make !last_make_index in
+  let f = Str.matched_group 1 !last_make
+  and l = int_of_string (Str.matched_group 2 !last_make)
+  and b = int_of_string (Str.matched_group 3 !last_make)
+  and e = int_of_string (Str.matched_group 4 !last_make)
+  and msg_index = Str.match_beginning ()
+  in 
+  last_make_index := Str.group_end 4; 
+  (f,l,b,e,
+   String.sub !last_make msg_index (String.length !last_make - msg_index))
+
+
 let main files = 
   (* Statup preferences *)
   load_pref ();
@@ -1738,16 +1726,7 @@ let main files =
   (* Menu bar *)
   let menubar = GMenu.menu_bar ~packing:vbox#pack () in
 
-  (* Tearable Toolbar *)
-(*
-  let handle = GBin.handle_box 
-		 ~show:!current.show_toolbar
-		 ~handle_position:`LEFT
-		 ~snap_edge:`LEFT
-		 ~packing:vbox#pack
-		 ()
-  in
-*)
+  (* Toolbar *)
   let toolbar = GButton.toolbar 
 		  ~orientation:`HORIZONTAL 
 		  ~style:`ICONS
@@ -1756,10 +1735,6 @@ let main files =
 		     (vbox#pack ~expand:false ~fill:false)
 		  ()
   in
-(*
-  show_toolbar := 
-  (fun b -> if b then handle#misc#show () else handle#misc#hide ());
-*)
   show_toolbar := 
   (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ());
 
@@ -1773,6 +1748,7 @@ let main files =
 
   (* File/Load Menu *)
   let load f =
+    let f = absolute_filename f in		
     try
       prerr_endline "Loading file starts";
       Vector.find_or_fail 
@@ -1780,7 +1756,7 @@ let main files =
 	   | {analyzed_view=Some av} -> 
 	       (match av#filename with 
 		| None -> false 
-		| Some fn -> f=fn)
+		| Some fn -> same_file f fn)
 	   | _ -> false) 
 	!input_views;
       prerr_endline "Loading: must open";
@@ -1804,11 +1780,7 @@ let main files =
       prerr_endline "Loading: register view";
       (get_input_view index).analyzed_view <- Some av;
       prerr_endline "Loading: set filename";
-      av#set_filename 
-	(Some (if Filename.is_relative f then 
-		 Filename.concat initial_cwd f
-	       else f
-	      ));
+      av#set_filename (Some f);
       prerr_endline "Loading: stats";
       av#update_stats;
       let input_buffer = view#buffer in
@@ -1817,6 +1789,7 @@ let main files =
       input_buffer#place_cursor input_buffer#start_iter;
       prerr_endline ("Loading: switch to view "^ string_of_int index);
       set_current_view index;
+      set_tab_image index ~icon:`YES;
       prerr_endline "Loading: highlight";
       Highlight.highlight_all input_buffer;
       input_buffer#set_modified false;
@@ -2020,10 +1993,6 @@ let main files =
 	       (get_current_view()).view#buffer;
 	       (out_some (get_current_view()).analyzed_view)#recenter_insert));
 
-  (*  (* 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 () =
     save_pref();
@@ -2035,8 +2004,8 @@ let main files =
 	       ~default:0
 	       ~icon:
 	       (let img = GMisc.image () in
-		img#set_stock warning_icon;
-		img#set_icon_size dialog_size;
+		img#set_stock `DIALOG_WARNING;
+		img#set_icon_size `DIALOG;
 		img#coerce)
 	       "There are unsaved buffers"
 	    )
@@ -2054,26 +2023,28 @@ let main files =
   let edit_menu = factory#add_submenu "_Edit" in
   let edit_f = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Edit/" edit_menu ~accel_group in
   ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback:
-	   (do_if_not_computing 
+	   (do_if_not_computing "undo"
 	      (fun () -> 
 		 ignore ((out_some ((get_current_view()).analyzed_view))#
 			   without_auto_complete 
 			   (fun () -> (get_current_view()).view#undo) ()))));
-  ignore(edit_f#add_item "_Clear Undo Stack" ~key:GdkKeysyms._exclam ~callback:
+  ignore(edit_f#add_item "_Clear Undo Stack" 
+	   (* ~key:GdkKeysyms._exclam *)
+	   ~callback:
 	   (fun () -> 
 	      ignore (get_current_view()).view#clear_undo));
   ignore(edit_f#add_separator ());
-  ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
-	   (fun () -> GtkSignal.emit_unit
-	      (get_current_view()).view#as_view 
-	      GtkText.View.S.copy_clipboard));
   ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
-	   (do_if_not_computing 
+	   (do_if_not_computing "cut"
 	      (fun () -> GtkSignal.emit_unit
 		 (get_current_view()).view#as_view 
 		 GtkText.View.S.cut_clipboard)));
+  ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
+	   (fun () -> GtkSignal.emit_unit
+	      (get_current_view()).view#as_view 
+	      GtkText.View.S.copy_clipboard));
   ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
-	   (do_if_not_computing
+	   (do_if_not_computing "paste"
 	      (fun () -> 
 		 try GtkSignal.emit_unit
 		   (get_current_view()).view#as_view 
@@ -2089,23 +2060,200 @@ let main files =
       ~callback:
    in
 *)
+(*
    auto_complete := 
    (fun b -> match (get_current_view()).analyzed_view with
       | Some av -> av#set_auto_complete b
       | None -> ());
-   let read_only_i = edit_f#add_check_item "Expert" ~active:false
-		      ~key:GdkKeysyms._B
-		      ~callback:(fun b -> ()
-				)
-  in
-  read_only_i#misc#set_state `INSENSITIVE;
+*)
 
+  let last_found = ref None in
+  let search_backward = ref false in
+  let find_w = GWindow.window 
+		 (* ~wm_class:"CoqIde" ~wm_name:"CoqIde" *)
+		 (* ~allow_grow:true ~allow_shrink:true *)
+		 (* ~width:!current.window_width ~height:!current.window_height *)
+		 ~position:`CENTER
+		 ~title:"CoqIde search/replace" ()
+  in
+  let find_box = GPack.table
+		   ~columns:3 ~rows:3
+		   ~col_spacings:10 ~row_spacings:10 ~border_width:10
+		   ~homogeneous:false ~packing:find_w#add () in
+  
+  let find_lbl = 
+    GMisc.label ~text:"Find:"
+      ~xalign:1.0
+      ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) () 
+  in
+  let find_entry = GEdit.entry
+		     ~editable: true
+		     ~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X)
+		     ()
+  in
+  let replace_lbl = 
+    GMisc.label ~text:"Replace with:"
+      ~xalign:1.0
+      ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) () 
+  in
+  let replace_entry = GEdit.entry
+			~editable: true
+			~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X)
+			()
+  in
+  let case_sensitive_check = 
+    GButton.check_button
+      ~label:"case sensitive"
+      ~active:true
+      ~packing: (find_box#attach ~left:1 ~top:2)
+      ()
+  in
+(*
+  let find_backwards_check = 
+    GButton.check_button
+      ~label:"search backwards"
+      ~active:false
+      ~packing: (find_box#attach ~left:1 ~top:3)
+      ()
+  in
+*)
+  let close_find_button =
+    GButton.button
+      ~label:"Close"
+      ~packing: (find_box#attach ~left:2 ~top:0)
+      ()
+  in
+  let replace_button =
+    GButton.button
+      ~label:"Replace"
+      ~packing: (find_box#attach ~left:2 ~top:1)
+      ()
+  in
+  let replace_find_button =
+    GButton.button
+      ~label:"Replace and find"
+      ~packing: (find_box#attach ~left:2 ~top:2)
+      ()
+  in
+  let last_find () =
+    let v = (get_current_view()).view in
+    let b = v#buffer in
+    let start,stop =
+      match !last_found with 
+	| None -> let i = b#get_iter_at_mark `INSERT in (i,i)
+	| Some(start,stop) ->
+	    let start = b#get_iter_at_mark start
+	    and stop = b#get_iter_at_mark stop
+	    in
+	    b#remove_tag_by_name ~start ~stop "found";
+	    last_found:=None;
+	    start,stop
+    in
+    (v,b,start,stop)
+  in
+  let do_replace () =
+    let v = (get_current_view()).view in
+    let b = v#buffer in
+    match !last_found with 
+      | None -> ()
+      | Some(start,stop) ->
+	  let start = b#get_iter_at_mark start
+	  and stop = b#get_iter_at_mark stop
+	  in
+	  b#delete ~start ~stop;
+	  b#insert ~iter:start replace_entry#text;
+	  last_found:=None
+  in
+  let find_from (v : Undo.undoable_view)
+    (b : GText.buffer) (starti : GText.iter) text =
+    prerr_endline ("Searching for " ^ text);
+    match (if !search_backward then starti#backward_search text
+	   else starti#forward_search text)
+    with
+      | None -> ()
+      | Some(start,stop) ->
+	  b#apply_tag_by_name "found" ~start ~stop;
+	  let start = `MARK (b#create_mark start)
+	  and stop = `MARK (b#create_mark stop)
+	  in
+	  v#scroll_to_mark ~use_align:false ~yalign:0.75 ~within_margin:0.25
+	    stop;
+	  last_found := Some(start,stop)
+  in
+  let do_find () =
+    let (v,b,starti,_) = last_find () in
+    find_from v b starti find_entry#text 
+  in
+  let do_replace_find () =
+    do_replace();
+    do_find()
+  in
+  let close_find () =
+    let (v,b,_,stop) = last_find () in
+    b#place_cursor stop;
+    find_w#misc#hide();
+    v#coerce#misc#grab_focus()
+  in
+  let key_find ev =
+    let s = GdkEvent.Key.state ev and k = GdkEvent.Key.keyval ev in
+    if k = GdkKeysyms._Escape then
+      begin
+	let (v,b,_,stop) = last_find () in
+	find_w#misc#hide();
+	v#coerce#misc#grab_focus();
+	true
+      end 
+    else if k = GdkKeysyms._Return then
+      begin
+	close_find();
+	true
+      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;
+	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;
+	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 ();
+    find_w#present ();
+    find_entry#misc#grab_focus ()
+  in
+  let find_i = edit_f#add_item "_Find in buffer"
+		 ~key:GdkKeysyms._F
+		 ~callback:(find_f ~backward:false)
+  in
+  let find_back_i = edit_f#add_item "_Find backwards"
+		 ~key:GdkKeysyms._B
+		 ~callback:(find_f ~backward:true)
+  in
+(*
   let search_if = edit_f#add_item "Search _forward"
 		    ~key:GdkKeysyms._greater
   in
   let search_ib = edit_f#add_item "Search _backward"
 		    ~key:GdkKeysyms._less
   in
+*)
 (*
   let complete_i = edit_f#add_item "_Complete"
 		     ~key:GdkKeysyms._comma
@@ -2121,23 +2269,29 @@ let main files =
   complete_i#misc#set_state `INSENSITIVE;
 *)
   
-  ignore(edit_f#add_item "Complete" ~key:GdkKeysyms._slash ~callback:
-	 (do_if_not_computing 
+  ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback:
+	 (do_if_not_computing "complete word"
 	    (fun () -> 
 	       ignore (
 		 let av = out_some ((get_current_view()).analyzed_view) in 
 		 av#complete_at_offset (av#get_insert)#offset
 	    ))));
 
-  to_do_on_page_switch := 
-  (fun i -> 
-     prerr_endline ("Switching to tab "^(string_of_int i));
-     let v = out_some (get_input_view i).analyzed_view in
-     read_only_i#set_active v#read_only
-  )::!to_do_on_page_switch;
-  
-
   ignore(edit_f#add_separator ());
+  (* external editor *)
+  let _ = 
+    edit_f#add_item "External editor" ~key:GdkKeysyms._E ~callback:
+      (fun () -> 	 
+	 let av = out_some ((get_current_view()).analyzed_view) in 
+	 match av#filename with
+	   | None -> ()
+	   | Some f ->
+	       save_f ();
+	       let l,r = !current.cmd_editor in
+	       let _ = run_command av#insert_message (l ^ f ^ r) in
+	       av#revert)
+  in
+  let _ = edit_f#add_separator () in
   (* Preferences *)
   let reset_revert_timer () =
     disconnect_revert_timer ();
@@ -2146,7 +2300,7 @@ let main files =
 	(GMain.Timeout.add ~ms:!current.global_auto_revert_delay 
 	   ~callback:
 	   (fun () -> 
-	      do_if_not_computing (fun () -> revert_f ()) ();
+	      do_if_not_computing "revert" (fun () -> revert_f ()) ();
 	      true))
   in reset_revert_timer (); (* to enable statup preferences timer *)
 
@@ -2169,7 +2323,7 @@ let main files =
 	(GMain.Timeout.add ~ms:!current.auto_save_delay 
 	   ~callback:
 	   (fun () -> 
-	      do_if_not_computing (fun () -> auto_save_f ()) ();
+	      do_if_not_computing "autosave" (fun () -> auto_save_f ()) ();
 	      true))
   in reset_auto_save_timer (); (* to enable statup preferences timer *)
 
@@ -2206,7 +2360,7 @@ let main files =
   in
 
   let do_or_activate f = 
-    do_if_not_computing (do_or_activate (fun av -> f av ; !pop_info();!push_info (Coq.current_status())))
+    do_if_not_computing "do_or_activate" (do_or_activate (fun av -> f av ; !pop_info();!push_info (Coq.current_status())))
   in
 
   let add_to_menu_toolbar text ~tooltip ~key ~callback icon = 
@@ -2281,8 +2435,9 @@ let main files =
     let analyzed_view = out_some current.analyzed_view in
     if analyzed_view#is_active then ignore (f analyzed_view)
   in
-  let do_if_active f = do_if_not_computing (do_if_active_raw f) in
+  let do_if_active f = do_if_not_computing "do_if_active" (do_if_active_raw f) in
 
+(*
   let blaster_i = 
     tactics_factory#add_item "_Blaster"
 	    ~key:GdkKeysyms._b
@@ -2290,6 +2445,7 @@ let main files =
 	    (* Custom locking mechanism! *)
   in
   blaster_i#misc#set_state `INSENSITIVE;
+*)
  
   ignore (tactics_factory#add_item "_auto" 
 	    ~key:GdkKeysyms._a
@@ -2353,6 +2509,43 @@ let main files =
 				    ))
 	 );
   
+  ignore (tactics_factory#add_separator ());
+  let add_simple_template (factory: GMenu.menu GMenu.factory) 
+    (menu_text, text) =
+    let text = 
+      let l = String.length text - 1 in
+      if String.get text l = '.'
+      then text ^"\n"
+      else text ^" "
+    in
+    ignore (factory#add_item menu_text
+	      ~callback:
+	      (do_if_not_computing "simple template"
+		 (fun () -> let {view = view } = get_current_view () in
+		  ignore (view#buffer#insert_interactive text))))
+  in
+  List.iter 
+    (fun l -> 
+       match l with 
+       | [] -> ()
+       | [s] -> add_simple_template tactics_factory ("_"^s, s) 
+       | s::_ -> 
+	   let a = "_@..." in
+	   a.[1] <- s.[0];
+	   let f = tactics_factory#add_submenu a in 
+	   let ff = new GMenu.factory f ~accel_group in
+	   List.iter 
+	     (fun x -> 
+		add_simple_template
+		ff 
+		((String.sub x 0 1)^
+		 "_"^
+		 (String.sub x 1 (String.length x - 1)),
+		 x))
+	     l
+    ) 
+    Coq_commands.tactics;
+  
   (* Templates Menu *)
   let templates_menu =  factory#add_submenu "Te_mplates" in
   let templates_factory = new GMenu.factory templates_menu 
@@ -2362,7 +2555,7 @@ let main files =
   in
   let add_complex_template (menu_text, text, offset, len, key) =
     (* Templates/Lemma *)
-    let callback = do_if_not_computing 
+    let callback = do_if_not_computing "complex template"
 		     (fun () ->
 			let {view = view } = get_current_view () in
 			if view#buffer#insert_interactive text then begin
@@ -2401,14 +2594,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
       let cases = Coq.make_cases w
       in
       let print c = function
-	| [x] -> fprintf c "  | %s => _@\n" x
-	| x::l -> fprintf c "  | (%s%a) => _@\n" x 
-	      (print_list (fun c s -> fprintf c " %s" s)) l
+	| [x] -> Format.fprintf c "  | %s => _@\n" x
+	| x::l -> Format.fprintf c "  | (%s%a) => _@\n" x 
+	      (print_list (fun c s -> Format.fprintf c " %s" s)) l
 	| [] -> assert false
       in
       let b = Buffer.create 1024 in
-      let fmt = formatter_of_buffer b in
-      fprintf fmt "@[match var with@\n%aend@]@."
+      let fmt = Format.formatter_of_buffer b in
+      Format.fprintf fmt "@[match var with@\n%aend@]@."
 	(print_list print) cases;
       let s = Buffer.contents b in
       prerr_endline s;
@@ -2430,6 +2623,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 	    ~callback
 	 );
   
+(*
   let add_simple_template (factory: GMenu.menu GMenu.factory) 
     (menu_text, text) =
     let text = 
@@ -2440,22 +2634,23 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
     in
     ignore (factory#add_item menu_text
 	      ~callback:
-	      (do_if_not_computing 
+	      (do_if_not_computing "simple template"
 		 (fun () -> let {view = view } = get_current_view () in
 		  ignore (view#buffer#insert_interactive text))))
   in
+*)
   ignore (templates_factory#add_separator ());
 (*
   List.iter (add_simple_template templates_factory)
-    [ "_Auto", "Auto ";
-      "_Auto with *", "Auto with * ";
-      "_EAuto", "EAuto ";
-      "_EAuto with *", "EAuto with * ";
-      "_Intuition", "Intuition ";
-      "_Omega", "Omega ";
-      "_Simpl", "Simpl ";
-      "_Tauto", "Tauto ";
-      "Tri_vial", "Trivial ";
+    [ "_auto", "auto ";
+      "_auto with *", "auto with * ";
+      "_eauto", "eauto ";
+      "_eauto with *", "eauto with * ";
+      "_intuition", "intuition ";
+      "_omega", "omega ";
+      "_simpl", "simpl ";
+      "_tauto", "tauto ";
+      "tri_vial", "trivial ";
     ];
   ignore (templates_factory#add_separator ());
 *)
@@ -2518,7 +2713,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   let externals_menu =  factory#add_submenu "_Compile" in
   let externals_factory = new GMenu.factory externals_menu 
 			    ~accel_path:"<CoqIde MenuBar>/Compile/"
-			    ~accel_group in
+			    ~accel_group 
+			   ~accel_modi:[]
+  in
   
   (* Command/Compile Menu *)
   let compile_f () =
@@ -2543,30 +2740,68 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 	  av#insert_message res
 	end
   in
-  let compile_m = externals_factory#add_item "_Compile Buffer" ~callback:compile_f in
+  let compile_m = 
+    externals_factory#add_item "_Compile Buffer" ~callback:compile_f 
+  in
 
   (* Command/Make Menu *)
   let make_f () =
     let v = get_active_view () in
     let av = out_some v.analyzed_view in
+(*
     save_f ();
+*)
     av#insert_message "Command output:\n";
     let s,res = run_command av#insert_message !current.cmd_make in
     last_make := res;
+    last_make_index := 0;
     !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
   in
-  let make_m = externals_factory#add_item "_Make" ~callback:make_f in
+  let make_m = externals_factory#add_item "_Make" 
+		 ~key:GdkKeysyms._F6
+		 ~callback:make_f 
+  in
   
 
   (* Compile/Next Error *)
-  let next_error () = ()
+  let next_error () = 
+    try
+      let file,line,start,stop,error_msg = search_next_error () in
+      load file;
+      let v = get_current_view () in
+      let av = out_some v.analyzed_view in
+      let input_buffer = v.view#buffer in
 (*
-    let file,line,start,stop = search_next_error () in
-    av#insert_message 
-      ("Error in " ^ file ^ "," ^ (string_of_int line)
+      let init = input_buffer#start_iter in
+      let i = init#forward_lines (line-1) in
 *)
-  in
-  let next_error_m = externals_factory#add_item "_Next error" ~callback:next_error in
+(*
+  let convert_pos = byte_offset_to_char_offset phrase in
+  let start = convert_pos start in
+  let stop = convert_pos stop in
+*)
+(*
+      let starti = i#forward_chars start in
+      let stopi = i#forward_chars stop in
+*)
+      let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in
+      let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in
+      input_buffer#apply_tag_by_name "error"
+   	~start:starti
+	~stop:stopi;
+      input_buffer#place_cursor starti;
+      av#set_message error_msg;
+      v.view#misc#grab_focus ()
+    with Not_found ->
+      last_make_index := 0;
+      let v = get_current_view () in
+      let av = out_some v.analyzed_view in
+      av#set_message "No more errors.\n"
+  in
+  let next_error_m = 
+    externals_factory#add_item "_Next error" 
+      ~key:GdkKeysyms._F7
+      ~callback:next_error in
   
 
   (* Command/CoqMakefile Menu*)
@@ -2601,7 +2836,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   let detach_menu = configuration_factory#add_item 
 		      "Detach _Script Window"
 		      ~callback:
-		      (do_if_not_computing
+		      (do_if_not_computing "detach script window"
 			 (fun () -> 
 			    let nb = notebook () in
 			    if nb#misc#toplevel#get_oid=w#coerce#get_oid then
@@ -2616,38 +2851,39 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 			      end	      
 			 ))
   in
-  let detach_current_view = configuration_factory#add_item 
-			      "Detach _View"
-			      ~callback:
-			      (do_if_not_computing
-				 (fun () -> 
-				    match get_current_view () with  
-				    | {view=v;analyzed_view=Some av} -> 
-			      		let w = GWindow.window ~show:true 
-						  ~width:(!current.window_width/2)
-						  ~height:(!current.window_height)
-						  ~title:(match av#filename with
-							  | None -> "*Unnamed*"
-							  | Some f -> f) 
-						  () 
-					in
-					let sb = GBin.scrolled_window 
-						   ~packing:w#add () 
-					in
-					let nv = GText.view 
-						   ~buffer:v#buffer 
-						   ~packing:sb#add 
-						   ()
-					in
-					nv#misc#modify_font 
-					  !current.text_font; 
-					ignore (w#connect#destroy 
-						  ~callback:
-						  (fun () -> av#remove_detached_view w));
-					av#add_detached_view w
-				    | _ -> ()
-
-				 ))
+  let detach_current_view = 
+    configuration_factory#add_item 
+      "Detach _View"
+      ~callback:
+      (do_if_not_computing "detach view"
+	 (fun () -> 
+	    match get_current_view () with  
+	      | {view=v;analyzed_view=Some av} -> 
+		  let w = GWindow.window ~show:true 
+			    ~width:(!current.window_width/2)
+			    ~height:(!current.window_height)
+			    ~title:(match av#filename with
+				      | None -> "*Unnamed*"
+				      | Some f -> f) 
+			    () 
+		  in
+		  let sb = GBin.scrolled_window 
+			     ~packing:w#add () 
+		  in
+		  let nv = GText.view 
+			     ~buffer:v#buffer 
+			     ~packing:sb#add 
+			     ()
+		  in
+		  nv#misc#modify_font 
+		    !current.text_font; 
+		  ignore (w#connect#destroy 
+			    ~callback:
+			    (fun () -> av#remove_detached_view w));
+		  av#add_detached_view w
+	      | _ -> ()
+		  
+	 ))
   in
   (* Help Menu *)
 
@@ -2657,9 +2893,15 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		       ~accel_modi:[]
 		       ~accel_group in
   let _ = help_factory#add_item "Browse Coq _Manual" 
-	    ~callback:(fun () -> browse (!current.doc_url ^ "main.html")) in
+	    ~callback:
+	    (fun () -> 
+	       let av = out_some ((get_current_view ()).analyzed_view) in 
+	       browse av#insert_message (!current.doc_url ^ "main.html")) in
   let _ = help_factory#add_item "Browse Coq _Library" 
-	    ~callback:(fun () -> browse !current.library_url) in
+	    ~callback:
+	    (fun () -> 
+	       let av = out_some ((get_current_view ()).analyzed_view) in 
+	       browse av#insert_message !current.library_url) in
   let _ = 
     help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1
       ~callback:(fun () -> 
@@ -2667,7 +2909,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		   av#help_for_keyword ())
   in
   let _ = help_factory#add_separator () in
+(*
   let faq_m = help_factory#add_item "_FAQ" in
+*)
   let about_m = help_factory#add_item "_About" in
 
   (* End of menu *)
@@ -2776,10 +3020,11 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
     end;
     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
+    let iit = v#buffer#get_iter_at_mark `SEL_BOUND 
+    and insert_iter = v#buffer#get_iter_at_mark `INSERT
+    in
     prerr_endline ("SELBOUND="^(string_of_int iit#offset));
-    prerr_endline ("INSERT="^(string_of_int 
-				(v#buffer#get_iter_at_mark `INSERT)#offset));
+    prerr_endline ("INSERT="^(string_of_int insert_iter#offset));
     
     (match
        if !search_forward then iit#forward_search txt 
@@ -2847,6 +3092,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 	    ));
   ignore (search_input#entry#connect#changed search_f);
   
+(*
   ignore (search_if#connect#activate
 	    ~callback:(fun b -> 
 			 search_forward:= true;
@@ -2867,7 +3113,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 			 v#buffer#move_mark `SEL_BOUND old_sel;
 			 search_f ();
 		      ));
-
+*)
   let status_context = status_bar#new_context "Messages" in
   let flash_context = status_bar#new_context "Flash" in
   ignore (status_context#push "Ready");
@@ -2901,7 +3147,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   let _ = tv2#event#connect#motion_notify
 	    ~callback:
 	    (fun e -> 
-	       (do_if_not_computing
+	       (do_if_not_computing "motion notify"
 		  (fun e -> 
 		     let win = match tv2#get_window `WIDGET with
 		       | None -> assert false
@@ -2972,23 +3218,16 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   w#show ();
   message_view := Some tv3;
   proof_view := Some tv2;
-  let view = create_input_tab "*Unnamed Buffer*" in
-  let index = add_input_view {view = view;
-			      analyzed_view = None;
-			     }
-  in
-  (get_input_view index).analyzed_view <- Some (new analyzed_view index);
-  activate_input index;
-  set_tab_image index yes_icon;
-  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 () -> tv2#buffer#set_text ""; about tv2#buffer));
+(*
   ignore (faq_m#connect#activate 
 	    ~callback:(fun () -> 
 			 load (Filename.concat lib_ide "FAQ")));
   
+*)
   resize_window := (fun () -> 
 		      w#resize 
 		      ~width:!current.window_width
@@ -3028,13 +3267,28 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		end;
 	      false;
 	   ));
-  List.iter (fun f -> 
-	       if Sys.file_exists f then load f else 
-		 if (let l = String.length f in 
-		     l >= 3 && String.sub f (l-3) 2 = ".v") 
-		 then load f 
-		 else load (f^".v")) files;
-  if List.length files >=1 then activate_input 1
+  if List.length files >=1 then
+    begin
+      List.iter (fun f -> 
+		   if Sys.file_exists f then load f else 
+		     if Filename.check_suffix f ".v" 
+		     then load f 
+		     else load (f^".v")) files;
+      activate_input 0
+    end
+  else
+    begin
+      let view = create_input_tab "*Unnamed Buffer*" in
+      let index = add_input_view {view = view;
+				  analyzed_view = None;
+				 }
+      in
+      (get_input_view index).analyzed_view <- Some (new analyzed_view index);
+      activate_input index;
+      set_tab_image index ~icon:`YES;
+      view#misc#modify_font !current.text_font
+    end;
+
 ;;
 
 let start () = 
@@ -3065,3 +3319,4 @@ let start () =
 	  flush stderr;
 	  crash_save 127
   done
+
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index c42c01fe2..db0f82b16 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -127,35 +127,6 @@ let try_export file_name s =
   true
   with e -> prerr_endline (Printexc.to_string e);false
 
-let browse url =
-  let l,r = !current.cmd_browse in
-  ignore (Sys.command (l ^ url ^ r))
-
-let url_for_keyword =
-  let ht = Hashtbl.create 97 in
-  begin try
-    let cin = open_in (Filename.concat lib_ide "index_urls.txt") in
-    try while true do
-      let s = input_line cin in
-      try 
-	let i = String.index s ',' in
-	let k = String.sub s 0 i in
-	let u = String.sub s (i + 1) (String.length s - i - 1) in
-	Hashtbl.add ht k u
-      with _ ->
-	()
-    done with End_of_file ->
-      close_in cin
-  with _ ->
-    ()
-  end;
-  (Hashtbl.find ht : string -> string)
-
-
-let browse_keyword text = 
-  try let u = url_for_keyword text in browse (!current.doc_url ^ u) 
-  with _ -> ()
-
 let my_stat f = try Some (Unix.stat f) with _ -> None
 
 let revert_timer = ref None
@@ -274,6 +245,37 @@ let run_command f c =
   done;
   (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
 
+let browse f url =
+  let l,r = !current.cmd_browse in
+  let (s,res) = run_command f (l ^ url ^ r) in
+  ()
+
+let url_for_keyword =
+  let ht = Hashtbl.create 97 in
+  begin try
+    let cin = open_in (Filename.concat lib_ide "index_urls.txt") in
+    try while true do
+      let s = input_line cin in
+      try 
+	let i = String.index s ',' in
+	let k = String.sub s 0 i in
+	let u = String.sub s (i + 1) (String.length s - i - 1) in
+	Hashtbl.add ht k u
+      with _ ->
+	()
+    done with End_of_file ->
+      close_in cin
+  with _ ->
+    ()
+  end;
+  (Hashtbl.find ht : string -> string)
+
+
+let browse_keyword f text = 
+  try let u = url_for_keyword text in browse f (!current.doc_url ^ u) 
+  with _ -> ()
+
+
 let underscore = Glib.Utf8.to_unichar "_" (ref 0)
 
 let arobase = Glib.Utf8.to_unichar "@" (ref 0)
@@ -281,3 +283,24 @@ let prime = Glib.Utf8.to_unichar "'" (ref 0)
 let bn = Glib.Utf8.to_unichar "\n" (ref 0)
 let space = Glib.Utf8.to_unichar " " (ref 0)
 let tab = Glib.Utf8.to_unichar "\t" (ref 0)
+
+
+(*
+  checks if two file names refer to the same (existing) file
+*)
+
+let same_file f1 f2 =
+  try
+    let s1 = Unix.stat f1
+    and s2 = Unix.stat f2 
+    in
+    (s1.Unix.st_dev = s2.Unix.st_dev) &&
+    (s1.Unix.st_ino = s2.Unix.st_ino) 
+  with
+      Unix.Unix_error _ -> false
+
+let absolute_filename f =
+  if Filename.is_relative f then 
+    Filename.concat (Sys.getcwd ()) f
+  else f
+	      
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index bf1915978..08c392a91 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -9,8 +9,8 @@
 (* $Id$ *)
 
 val async : ('a -> unit) -> 'a -> unit
-val browse : string -> unit
-val browse_keyword : string -> unit
+val browse : (string -> unit) -> string -> unit
+val browse_keyword : (string -> unit) -> string -> unit
 val byte_offset_to_char_offset : string -> int -> int
 val clear_stdout : unit -> unit
 val debug : bool ref
@@ -65,3 +65,15 @@ val flash_info : (?delay:int -> string -> unit) ref
 val set_location : (string -> unit) ref
 
 val pulse : (unit -> unit) ref
+
+
+(*
+  checks if two file names refer to the same (existing) file
+*)
+
+val same_file : string -> string -> bool
+
+(*
+  returns an absolute filename equivalent to given filename
+*)
+val absolute_filename : string -> string
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 7b76eafc0..ad0c19743 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -80,6 +80,7 @@ type pref =
       mutable modifiers_valid : Gdk.Tags.modifier list;
 
       mutable cmd_browse : string * string;
+      mutable cmd_editor : string * string;
 
       mutable text_font : Pango.font_description;
 
@@ -127,6 +128,7 @@ let (current:pref ref) =
 
     
     cmd_browse = "netscape -remote \"OpenURL(", ")\"";
+    cmd_editor = "emacs ", "";
     
     text_font = Pango.Font.from_string "Monospace 12";
 
@@ -191,6 +193,7 @@ let save_pref () =
     add "modifiers_valid" 
       (List.map mod_to_str p.modifiers_valid) ++
     add "cmd_browse" [fst p.cmd_browse; snd p.cmd_browse] ++
+    add "cmd_editor" [fst p.cmd_editor; snd p.cmd_editor] ++
 
     add "text_font" [Pango.Font.to_string p.text_font] ++
 
@@ -244,6 +247,7 @@ let load_pref () =
     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_pair "cmd_editor" (fun v1 v2 -> np.cmd_editor <- (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);
@@ -431,6 +435,26 @@ let configure () =
       ""
   in
 
+  let cmd_editor = 
+    string
+      ~f:(fun s -> 
+	    !current.cmd_editor <- 
+	    try 
+	      let i = String.index s '%' in
+	      let pre = (String.sub s 0 i) in
+	      if String.length s - 1 = i then 
+		pre,""
+	      else
+		let post = String.sub s (i+2) (String.length s - i - 2) in
+		prerr_endline pre;
+		prerr_endline post;
+		pre,post
+	    with Not_found -> s,""
+	    )
+      ~help:"(%s for file name)" 
+      "External editor"
+      ((fst !current.cmd_editor)^"%s"^(snd !current.cmd_editor))
+  in    
   let cmd_browse = 
     string
       ~f:(fun s -> 
@@ -491,6 +515,7 @@ let configure () =
 *)
      Section("Externals",
 	     [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;
+	      cmd_editor;
 	      cmd_browse;doc_url;library_url]);
      Section("Tactics Wizard",
 	     [automatic_tactics]);
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 793b65f20..6cdfbcee2 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -35,6 +35,7 @@ type pref =
       mutable modifiers_valid : Gdk.Tags.modifier list;
 
       mutable cmd_browse : string * string;
+      mutable cmd_editor : string * string;
 
       mutable text_font : Pango.font_description;
 
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index b6f6550bd..d359d3d70 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1039,6 +1039,7 @@ let edit ?(with_apply=true)
     conf_struct_list =
   let return = ref Return_cancel in
   let window = GWindow.window
+		 ~position:`CENTER
       ~modal: true ~title: title
       ~width: width ~height: height ()
   in
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index cd6a5078a..a787b1e78 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -100,7 +100,7 @@ let files_to_link userfiles =
   let toplevel_objs =
     if !top then topobjs else if !opt then notopobjs else [] in
   let ide_objs = if !coqide then 
-    "threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
+    "str.cma"::"threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
   else [] 
   in
   let objs = 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index bdb5e68d4..f339f8d68 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -302,7 +302,7 @@ let init is_ide =
   if !batch_mode then (flush_all(); Profile.print_profile (); exit 0);
   Lib.declare_initial_state ()
 
-let init_ide () = init true; !ide_args
+let init_ide () = init true; List.rev !ide_args
 
 let start () =
   init false;