coqide: fenetre de cmmandes . undo correct

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

10 files changed, 467 insertions, 214 deletions

diff --git a/.depend b/.depend
index 6774baca7..aa7777953 100644
--- a/.depend
+++ b/.depend
@@ -454,6 +454,8 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
     pretyping/termops.cmx kernel/univ.cmx 
 doc/parse.cmo: parsing/ast.cmi 
 doc/parse.cmx: parsing/ast.cmx 
+ide/command_windows.cmo: ide/coq.cmi ide/coq_commands.cmo ide/ideutils.cmo 
+ide/command_windows.cmx: ide/coq.cmx ide/coq_commands.cmx ide/ideutils.cmx 
 ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
     tactics/hipattern.cmi ide/ideutils.cmo library/lib.cmi kernel/names.cmi \
@@ -470,18 +472,20 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
     proofs/refiner.cmx library/states.cmx proofs/tacmach.cmx kernel/term.cmx \
     lib/util.cmx toplevel/vernac.cmx toplevel/vernacentries.cmx \
     toplevel/vernacexpr.cmx ide/coq.cmi 
-ide/coqide.cmo: ide/coq.cmi ide/coq_commands.cmo ide/find_phrase.cmo \
-    ide/highlight.cmo ide/ideutils.cmo proofs/pfedit.cmi lib/pp_control.cmi \
+ide/coqide.cmo: ide/command_windows.cmo ide/coq.cmi ide/coq_commands.cmo \
+    ide/find_phrase.cmo ide/highlight.cmo ide/ideutils.cmo proofs/pfedit.cmi \
     ide/preferences.cmo ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo 
-ide/coqide.cmx: ide/coq.cmx ide/coq_commands.cmx ide/find_phrase.cmx \
-    ide/highlight.cmx ide/ideutils.cmx proofs/pfedit.cmx lib/pp_control.cmx \
+ide/coqide.cmx: ide/command_windows.cmx ide/coq.cmx ide/coq_commands.cmx \
+    ide/find_phrase.cmx ide/highlight.cmx ide/ideutils.cmx proofs/pfedit.cmx \
     ide/preferences.cmx ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx 
 ide/find_phrase.cmo: ide/ideutils.cmo 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmo 
 ide/highlight.cmx: ide/ideutils.cmx 
-ide/ideutils.cmo: config/coq_config.cmi lib/options.cmi ide/preferences.cmo 
-ide/ideutils.cmx: config/coq_config.cmx lib/options.cmx ide/preferences.cmx 
+ide/ideutils.cmo: config/coq_config.cmi lib/options.cmi lib/pp_control.cmi \
+    ide/preferences.cmo 
+ide/ideutils.cmx: config/coq_config.cmx lib/options.cmx lib/pp_control.cmx \
+    ide/preferences.cmx 
 ide/preferences.cmo: ide/config_lexer.cmo ide/utils/configwin.cmi 
 ide/preferences.cmx: ide/config_lexer.cmx ide/utils/configwin.cmx 
 ide/undo.cmo: ide/ideutils.cmo ide/undo.cmi 
diff --git a/Makefile b/Makefile
index 999320dff..ad5f5a59f 100644
--- a/Makefile
+++ b/Makefile
@@ -445,9 +445,10 @@ COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \
 	  ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \
 	  ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \
 	  ide/utils/configwin.cmo ide/config_lexer.cmo ide/preferences.cmo \
-	  ide/ideutils.cmo ide/undo.cmo ide/find_phrase.cmo \
+	  ide/ideutils.cmo ide/undo.cmo \
+	  ide/find_phrase.cmo \
           ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \
-	  ide/coq_tactics.cmo ide/coqide.cmo
+	  ide/coq_tactics.cmo  ide/command_windows.cmo ide/coqide.cmo
 
 COQIDECMX=$(COQIDECMO:.cmo=.cmx)
 COQIDEFLAGS=-I +lablgtk2
@@ -466,19 +467,19 @@ $(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(COQIDECMO)
 	$(COQMKTOP) -g -ide -top $(COQIDEFLAGS) lablgtk.cma $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ $(COQIDECMO)
 
 ide/%.cmo: ide/%.ml
-	$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+	$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
 ide/%.cmi: ide/%.mli
-	$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+	$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
 ide/%.cmx: ide/%.ml
 	$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
 
 ide/utils/%.cmo: ide/%.ml
-	$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+	$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
 ide/utils/%.cmi: ide/%.mli
-	$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+	$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
 ide/utils/%.cmx: ide/%.ml
 	$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
diff --git a/ide/.coqiderc b/ide/.coqiderc
index 9e10620fb..65a6085d9 100644
--- a/ide/.coqiderc
+++ b/ide/.coqiderc
@@ -3,6 +3,7 @@ binding "text" {
 		   "move-cursor" (paragraphs,1,0)
 		   "cut-clipboard" ()	
 		}
+  bind "<ctrl>x" { }
 }
 class "GtkTextView" binding "text"
 
@@ -24,4 +25,5 @@ font_name = "Serif 10"
 class "GtkLabel" style "menu"
 
 gtk-key-theme-name = "Emacs"
+gtk-can-change-accels = 1
 
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
new file mode 100644
index 000000000..f442eac2b
--- /dev/null
+++ b/ide/command_windows.ml
@@ -0,0 +1,118 @@
+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
+		 ~title:"CoqIde Commands" ~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 factory = new GMenu.factory menubar
+  in
+  let accel_group = factory#accel_group in
+
+  let notebook = GPack.notebook ~scrollable:true 
+		   ~packing:(vbox#pack 
+			       ~expand:true
+			       ~fill:true
+			    ) 
+		   ()
+  in
+  let hide_menu = factory#add_item "_Hide Window" 
+		    ~callback:window#misc#hide
+  in
+  let new_page_menu = factory#add_item "_New Page" in
+  let kill_page_menu = 
+    factory#add_item "_Kill Page" 
+      ~callback:
+      (fun () -> notebook#remove_page notebook#current_page)
+  in
+object(self)
+  val window = window
+  val menubar = menubar
+  val new_page_menu = new_page_menu
+  val notebook = notebook
+  method window = window
+  method new_command ?command ?term () =
+    let frame = GBin.frame 
+		  ~shadow_type:`ETCHED_OUT
+		  ~packing:notebook#append_page
+		  ()
+    in
+    notebook#next_page ();
+    let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in
+    let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
+    let combo = GEdit.combo ~popdown_strings:Coq_commands.state_preserving
+		  ~use_arrows:`ALWAYS
+		  ~ok_if_empty:false
+		  ~value_in_list:true
+		  ~packing:hbox#pack
+		  ()
+    in
+    combo#entry#set_editable false;
+
+    let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in
+    entry#misc#set_can_default true;
+    let r_bin =
+      GBin.scrolled_window 
+	~vpolicy:`AUTOMATIC 
+	~hpolicy:`AUTOMATIC
+	~packing:(vbox#pack ~fill:true ~expand:true) () in
+    let result = GText.view ~packing:r_bin#add () in
+    result#misc#set_can_focus false;
+    result#set_editable false;
+    begin match command,term with 
+      | None,None -> ()
+      | Some c, None -> 
+	  combo#entry#set_text c
+	  
+      | Some c, Some t -> 
+	  combo#entry#set_text c;
+	  entry#set_text t
+
+      | None , Some t -> 
+	  entry#set_text t
+    end;
+    entry#misc#grab_focus ();
+    entry#misc#grab_default ();
+
+    let callback () =
+      let phrase = combo#entry#text ^ " " ^ entry#text ^" . " in
+      try 
+	ignore(Coq.interp phrase);
+	result#buffer#set_text (Ideutils.read_stdout ())
+      with e ->
+	let (s,loc) = Coq.process_exn e in
+	assert (Glib.Utf8.validate s);
+	result#buffer#set_text s
+    in
+    ignore (entry#connect#activate ~callback);
+    ignore (combo#entry#connect#activate ~callback);
+    self#window#present ()
+
+  initializer 
+    ignore (new_page_menu#connect#activate self#new_command);
+    ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));
+end
+
+let command_window = ref None
+
+let main () = command_window := Some (new command_window ())
+
+let command_window () = match !command_window with 
+  | None -> failwith "No command window."
+  | Some c -> c
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 773fe54f6..065627d89 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -1,23 +1,23 @@
 let commands = [
-  "Abort";
+  ["Abort";
   "Add Abstract Ring";
   "Add Abstract Semi Ring";
   "Add Field";
   "Add LoadPath";
   "Add ML Path";
   "Add Morphism";
-  "Add Printing If ident";
-  "Add Printing Let ident";
+  "Add Printing If";
+  "Add Printing Let";
   "Add Rec LoadPath";
   "Add Rec ML Path";
   "Add Ring";
   "Add Semi Ring";
   "Add Semi Ring";
   "Add Setoid";
-  "Axiom";
-  "Back";
-  "Begin Silent";
-  "Canonical Structure";
+  "Axiom";];
+  ["Back";
+  "Begin Silent";];
+  ["Canonical Structure";
   "Cd";
   "Chapter";
   "Check";
@@ -25,16 +25,16 @@ let commands = [
   "Coercion Local";
   "CoFixpoint";
   "CoInductive";
-  "Correctness";
-  "Declare ML Module";
+  "Correctness";];
+  ["Declare ML Module";
   "Defined";
   "Definition";
   "Derive Dependent Inversion";
   "Derive Dependent Inversion_clear";
   "Derive Inversion";
   "Derive Inversion_clear";
-  "Drop";
-  "End";
+  "Drop";];
+  ["End";
   "End Silent";
   "Eval";
   "Explicitation of implicit arguments";
@@ -44,15 +44,15 @@ let commands = [
   "Extraction Inline";
   "Extraction Language";
   "Extraction Module";
-  "Extraction NoInline";
-  "Fact";
+  "Extraction NoInline";];
+  ["Fact";
   "Fixpoint";
-  "Focus";
-  "Global Variable";
+  "Focus";];
+  ["Global Variable";
   "Goal";
-  "Grammar";
-  "Hint;
-    * Hint Constructors";
+  "Grammar";];
+  ["Hint";
+   "Hint Constructors";
   "Hint Unfold";
   "Hint";
   "Hint Rewrite";
@@ -62,27 +62,27 @@ let commands = [
   "Hints Immediate";
   "Hints Resolve";
   "Hints Unfold";
-  "Hypothesis";
-  "Identity Coercion";
+  "Hypothesis";];
+  ["Identity Coercion";
   "Implicit Arguments Off";
   "Implicit Arguments On";
   "Implicits";
   "Inductive";
   "Infix";
-  "Inspect";
-  "Lemma";
+  "Inspect";];
+  ["Lemma";
   "Load";
   "Load Verbose";
   "Local";
   "Locate";
   "Locate File";
-  "Locate Library";
-  "Module";
+  "Locate Library";];
+  ["Module";
   "Module Type";
-  "Mutual Inductive";
-  "Notation";
-  "Opaque";
-  "Parameter";
+  "Mutual Inductive";];
+  ["Notation";];
+  ["Opaque";];
+  ["Parameter";
   "Print";
   "Print All";
   "Print Classes";
@@ -103,17 +103,17 @@ let commands = [
   "Print Table Printing If";
   "Print Table Printing Let";
   "Proof";
-  "Pwd";
-  "Qed";
-  "Quit";
-  "Read Module";
+  "Pwd";];
+  ["Qed";
+  "Quit";];
+  ["Read Module";
   "Record";
   "Recursive Extraction";
   "Recursive Extraction Module";
   "Remark";
   "Remove LoadPath";
-  "Remove Printing If ident";
-  "Remove Printing Let ident";
+  "Remove Printing If";
+  "Remove Printing Let";
   "Require";
   "Require Export";
   "Reset";
@@ -121,8 +121,8 @@ let commands = [
   "Reset Initial";
   "Restart";
   "Restore State";
-  "Resume";
-  "Save";
+  "Resume";];
+[  "Save";
   "Scheme";
   "Search";
   "Search ... inside ...";
@@ -156,16 +156,16 @@ let commands = [
   "Structure";
   "Suspend";
   "Syntactic Definition";
-  "Syntax";
-  "Tactic Definition";
-  "Test Printing If ident";
-  "Test Printing Let ident";
+  "Syntax";];
+  ["Tactic Definition";
+  "Test Printing If";
+  "Test Printing Let";
   "Test Printing Synth";
   "Test Printing Wildcard";
   "Theorem";
   "Time";
-  "Transparent";
-  "Undo";
+  "Transparent";];
+  ["Undo";
   "Unfocus";
   "Unset Extraction AutoInline";
   "Unset Extraction Optimize";
@@ -175,8 +175,71 @@ let commands = [
   "Unset Printing Coercions";
   "Unset Printing Synth";
   "Unset Printing Wildcard";
-  "Unset Undo";
-  "Variable";
-  "Variables";
-  "Write State";
+  "Unset Undo";];
+  ["Variable";
+  "Variables";];
+  ["Write State";];
+]
+
+let state_preserving = [
+  "Check";
+  "Eval";
+  "Extract Constant";
+  "Extract Inductive";
+  "Extraction";
+  "Extraction Inline";
+  "Extraction Language";
+  "Extraction Module";
+  "Extraction NoInline";
+  "Inspect";
+  "Print";
+  "Print All";
+  "Print Classes";
+  "Print Coercion Paths";
+  "Print Coercions";
+  "Print Extraction Inline";
+  "Print Graph";
+  "Print Hint";
+  "Print HintDb";
+  "Print LoadPath";
+  "Print ML Modules";
+  "Print ML Path";
+  "Print Module";
+  "Print Module Type";
+  "Print Modules";
+  "Print Proof";
+  "Print Section";
+  "Print Table Printing If";
+  "Print Table Printing Let";
+
+  "Pwd";
+
+  "Search";
+  "SearchAbout";
+  "SearchPattern";
+  "SearchRewrite";
+
+  "Set Printing Coercion";
+  "Set Printing Coercions";
+  "Set Printing Synth";
+  "Set Printing Wildcard";
+
+  "Show";
+  "Show Conjectures";
+  "Show Implicits";
+  "Show Intro";
+  "Show Intros";
+  "Show Proof";
+  "Show Script";
+  "Show Tree";
+
+  "Test Printing If";
+  "Test Printing Let";
+  "Test Printing Synth";
+  "Test Printing Wildcard";
+
+  "Unset Printing Coercion";
+  "Unset Printing Coercions";
+  "Unset Printing Synth";
+  "Unset Printing Wildcard";
 ]
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 657a0ff1e..c3f92d609 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3,7 +3,7 @@ open Vernacexpr
 open Coq
 open Ideutils
 
-let out_some s = match s with | None -> assert false | Some f -> f
+let out_some s = match s with | None -> failwith "toto" | Some f -> f
 
 let cb_ = ref None
 let cb () = out_some !cb_
@@ -110,6 +110,8 @@ type 'a viewable_script =
      mutable analyzed_view : 'a option;
     }
 
+
+
 class type analyzed_views = 
 object('self)
     val mutable act_id : GtkSignal.id option
@@ -127,6 +129,7 @@ object('self)
     val mutable read_only : bool
     val mutable filename : string option
     val mutable stats : Unix.stats option
+    method view : Undo.undoable_view
     method filename : string option
     method stats :  Unix.stats option
     method set_filename : string option -> unit
@@ -231,6 +234,21 @@ let remove_current_view_page () =
   kill_input_view c;
   ((notebook ())#get_nth_page c)#misc#hide ()
 
+
+let get_current_word () =
+  let av = out_some ((get_current_view ()).analyzed_view) in 
+  match GtkBase.Clipboard.wait_for_text (cb ()) with
+    | None -> 
+	prerr_endline "None selected";
+	let it = av#get_insert in
+	let start = it#backward_word_start in
+	let stop = start#forward_word_end in
+	av#view#buffer#get_text ~slice:true ~start ~stop ()
+    | Some t ->
+ 	prerr_endline "Some selected";
+	prerr_endline t;
+	t
+	  
 let status = ref None
 let push_info = ref (function s -> failwith "not ready")
 let pop_info = ref (function s -> failwith "not ready")
@@ -337,16 +355,6 @@ let break () = Unix.kill pid Sys.sigusr1
 let can_break () = set_break () 
 let cant_break () = unset_break () 
 
-(* Get back the standard coq out channels *)
-let read_stdout,clear_stdout =
-  let out_buff = Buffer.create 100 in
-  Pp_control.std_ft := Format.formatter_of_buffer out_buff;
-  (fun () -> Format.pp_print_flush !Pp_control.std_ft (); 
-     let r = Buffer.contents out_buff in
-     Buffer.clear out_buff; r),
-  (fun () -> 
-     Format.pp_print_flush !Pp_control.std_ft (); Buffer.clear out_buff)
-
 let find_tag_limits (tag :GText.tag) (it:GText.iter) = 
     (if not (it#begins_tag (Some tag)) 
      then it#backward_to_tag_toggle (Some tag)
@@ -383,6 +391,7 @@ object(self)
   val mutable read_only = false
   val mutable filename = None 
   val mutable stats = None
+  method view = input_view
   method filename = filename
   method stats = stats
   method set_filename f = 
@@ -401,21 +410,21 @@ object(self)
       | Some f -> begin
 	  let do_revert () = begin
 	    !push_info "Reverting buffer";
-	      try
-		if is_active then self#reset_initial;
-		let b = Buffer.create 1024 in
-		with_file f ~f:(input_channel b);
-		let s = try_convert (Buffer.contents b) in
-		input_buffer#set_text s;
-		self#update_stats;
-		input_buffer#place_cursor input_buffer#start_iter;
-		input_buffer#set_modified false;
-		!pop_info ();
-		!flash_info "Buffer reverted";
-		Highlight.highlight_all input_buffer;
-	      with _  -> 
-		!pop_info ();
-		!flash_info "Warning: could not revert buffer";
+	    try
+	      if is_active then self#reset_initial;
+	      let b = Buffer.create 1024 in
+	      with_file f ~f:(input_channel b);
+	      let s = try_convert (Buffer.contents b) in
+	      input_buffer#set_text s;
+	      self#update_stats;
+	      input_buffer#place_cursor input_buffer#start_iter;
+	      input_buffer#set_modified false;
+	      !pop_info ();
+	      !flash_info "Buffer reverted";
+	      Highlight.highlight_all input_buffer;
+	    with _  -> 
+	      !pop_info ();
+	      !flash_info "Warning: could not revert buffer";
 	  end
 	  in
 	  if input_buffer#modified then 
@@ -439,7 +448,7 @@ object(self)
 	  else do_revert () 
 	end
       | None -> ()
-      
+	  
   method save f = 
     filename <- Some f;
     try_export f (input_buffer#get_text ());
@@ -485,85 +494,85 @@ object(self)
 	      let tag = proof_buffer#create_tag []
 	      in 
 	      ignore
-	      (tag#connect#event ~callback:
-		 (fun ~origin ev it ->
-		    
-		    match GdkEvent.get_type ev with 
-		      | `BUTTON_PRESS -> 
-			  let ev = (GdkEvent.Button.cast ev) in
-			  if (GdkEvent.Button.button ev) = 3
-			  then begin 
-			    let loc_menu = GMenu.menu () in
-			    let factory = new GMenu.factory loc_menu in
-			    let add_coq_command (cp,ip) = 
-			      ignore (factory#add_item cp 
-					~callback:
-					(fun () -> ignore
-					   (self#insert_this_phrase_on_success 
-					      true
-					      true 
-					      false 
-					      (ip^"\n") 
-					      (ip^"\n"))
-					)
-				     )
-			    in
-			    List.iter add_coq_command commands;
-			    loc_menu#popup 
-			      ~button:3
-			      ~time:(GdkEvent.Button.time ev);
-			  end
-		      | `MOTION_NOTIFY -> 
-			  proof_buffer#remove_tag
-			  ~start:proof_buffer#start_iter
-			  ~stop:proof_buffer#end_iter
-			  last_shown_area;
-			  prerr_endline "Before find_tag_limits";
-			  let s,e = find_tag_limits tag 
-				      (new GText.iter it) 
-			  in
-			  prerr_endline "Apres find_tag_limits";
-			  proof_buffer#apply_tag 
-			    ~start:s 
-			    ~stop:e 
+		(tag#connect#event ~callback:
+		   (fun ~origin ev it ->
+		      
+		      match GdkEvent.get_type ev with 
+			| `BUTTON_PRESS -> 
+			    let ev = (GdkEvent.Button.cast ev) in
+			    if (GdkEvent.Button.button ev) = 3
+			    then begin 
+			      let loc_menu = GMenu.menu () in
+			      let factory = new GMenu.factory loc_menu in
+			      let add_coq_command (cp,ip) = 
+				ignore (factory#add_item cp 
+					  ~callback:
+					  (fun () -> ignore
+					     (self#insert_this_phrase_on_success 
+						true
+						true 
+						false 
+						(ip^"\n") 
+						(ip^"\n"))
+					  )
+				       )
+			      in
+			      List.iter add_coq_command commands;
+			      loc_menu#popup 
+				~button:3
+				~time:(GdkEvent.Button.time ev);
+			    end
+			| `MOTION_NOTIFY -> 
+			    proof_buffer#remove_tag
+			    ~start:proof_buffer#start_iter
+			    ~stop:proof_buffer#end_iter
 			    last_shown_area;
-			  prerr_endline "Applied tag";
-			  ()
-		      | _ -> ())
-	      );
+			    prerr_endline "Before find_tag_limits";
+			    let s,e = find_tag_limits tag 
+					(new GText.iter it) 
+			    in
+			    prerr_endline "Apres find_tag_limits";
+			    proof_buffer#apply_tag 
+			      ~start:s 
+			      ~stop:e 
+			      last_shown_area;
+			    prerr_endline "Applied tag";
+			    ()
+			| _ -> ())
+		);
 	      tag
-	  in
-	  List.iter
-	    (fun ((_,_,_,(s,_)) as hyp) -> 
-	       let tag = coq_menu (hyp_menu hyp) in
-	       proof_buffer#insert ~tags:[tag] (s^"\n"))
-	    hyps;
-	  proof_buffer#insert ("---------------------------------------(1/"^
-			       (string_of_int goal_nb)^
-			       ")\n") 
-	  ;
-	  let tag = coq_menu (concl_menu concl) in
-	  let _,_,_,sconcl = concl in
-	  proof_buffer#insert ~tags:[tag] sconcl;
-	  proof_buffer#insert "\n";
-	  let my_mark = `NAME "end_of_conclusion" in
-	  proof_buffer#move_mark
-	    ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
-	  proof_buffer#insert "\n\n";
-	  let i = ref 1 in
-	  List.iter 
-	    (function (_,(_,_,_,concl)) -> 
-	       incr i;
-	       proof_buffer#insert ("--------------------------------------("^
-				    (string_of_int !i)^
-				    "/"^
-				    (string_of_int goal_nb)^
-				    ")\n");
-	       proof_buffer#insert concl;
-	       proof_buffer#insert "\n\n";
-	    )
-	    r;
-	  ignore (proof_view#scroll_to_mark my_mark) 
+	    in
+	    List.iter
+	      (fun ((_,_,_,(s,_)) as hyp) -> 
+		 let tag = coq_menu (hyp_menu hyp) in
+		 proof_buffer#insert ~tags:[tag] (s^"\n"))
+	      hyps;
+	    proof_buffer#insert ("---------------------------------------(1/"^
+				 (string_of_int goal_nb)^
+				 ")\n") 
+	    ;
+	    let tag = coq_menu (concl_menu concl) in
+	    let _,_,_,sconcl = concl in
+	    proof_buffer#insert ~tags:[tag] sconcl;
+	    proof_buffer#insert "\n";
+	    let my_mark = `NAME "end_of_conclusion" in
+	    proof_buffer#move_mark
+	      ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
+	    proof_buffer#insert "\n\n";
+	    let i = ref 1 in
+	    List.iter 
+	      (function (_,(_,_,_,concl)) -> 
+		 incr i;
+		 proof_buffer#insert ("--------------------------------------("^
+				      (string_of_int !i)^
+				      "/"^
+				      (string_of_int goal_nb)^
+				      ")\n");
+		 proof_buffer#insert concl;
+		 proof_buffer#insert "\n\n";
+	      )
+	      r;
+	    ignore (proof_view#scroll_to_mark my_mark) 
       with e -> prerr_endline (Printexc.to_string e)
 
   method send_to_coq phrase show_output show_error localize =
@@ -685,7 +694,8 @@ object(self)
 	  end;
 	  r
 
-  method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = 
+  method insert_this_phrase_on_success 
+    show_output show_msg localize coqphrase insertphrase = 
     match self#send_to_coq coqphrase show_output show_msg localize with
       | Some ast ->
 	  begin
@@ -702,7 +712,7 @@ object(self)
 	    let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
 	    push_phrase start_of_phrase_mark end_of_phrase_mark ast;
 	    self#show_goals;
-	    (try (match Coq.get_current_goals () with 
+	    (*try (match Coq.get_current_goals () with 
 		    | [] ->  
 			(match self#send_to_coq "Save.\n" true true true with
 			   | Some ast -> 
@@ -722,7 +732,7 @@ object(self)
 		      	       end
 			   | None -> ())
 		    | _ -> ())
-	     with _ -> ());
+	     with _ -> ()*)
 	    true
 	  end
       | None -> self#insert_message ("Unsuccesfully tried: "^coqphrase);
@@ -869,26 +879,28 @@ object(self)
 		 self#insert_this_phrase_on_success true false false cp ip) l)
 
   method active_keypress_handler k = 
-    if !coq_computing then true else
-      match GdkEvent.Key.state k with
-	| l when List.mem `MOD1 l ->
-	    let k = GdkEvent.Key.keyval k in
-	    if GdkKeysyms._Return=k
-	    then ignore(
-	      if (input_buffer#insert_interactive "\n") then
-		begin
-		  let i= self#get_insert#backward_word_start in
-		  input_buffer#place_cursor i;
-		  self#process_until_insert_or_error
-		end);
-	    true
-	| l when List.mem `CONTROL l -> 
-	    let k = GdkEvent.Key.keyval k in
-	    if GdkKeysyms._c=k
-	    then break ();
-	    false
-	| l -> false
-
+    if !coq_computing then true else 
+      let state = GdkEvent.Key.state k in
+      begin
+	match  state with
+	  | l when List.mem `MOD1 l ->
+	      let k = GdkEvent.Key.keyval k in
+	      if GdkKeysyms._Return=k
+	      then ignore(
+		if (input_buffer#insert_interactive "\n") then
+		  begin
+		    let i= self#get_insert#backward_word_start in
+		    input_buffer#place_cursor i;
+		    self#process_until_insert_or_error
+		  end);
+	      true
+	  | l when List.mem `CONTROL l -> 
+	      let k = GdkEvent.Key.keyval k in
+	      if GdkKeysyms._c=k
+	      then break ();
+	      false
+	  | l -> false
+      end
   method disconnected_keypress_handler k = 
     match GdkEvent.Key.state k with
       | l when List.mem `CONTROL l -> 
@@ -956,13 +968,9 @@ object(self)
 	   end;
 	 end;
 	 last_index <- not last_index;)
+  
+  method help_for_keyword () = browse_keyword (get_current_word ())
 
-  method help_for_keyword () =
-    let it = self#get_insert in
-    let start = it#backward_word_start in
-    let stop = start#forward_word_end in
-    let text = input_buffer#get_text ~slice:true ~start ~stop () in
-    browse_keyword text
   initializer 
     ignore (message_buffer#connect#after#insert_text
 	      ~callback:(fun it s -> ignore 
@@ -998,8 +1006,8 @@ object(self)
 	    else set_tab_image index yes_icon;
 	 ));
     ignore (input_view#connect#after#paste_clipboard
-	   ~callback:(fun () ->
-			prerr_endline "Paste occured"));
+	      ~callback:(fun () ->
+			   prerr_endline "Paste occured"));
     ignore (input_buffer#connect#changed
 	      ~callback:(fun () -> 
 			   let r = input_view#visible_rect in
@@ -1078,7 +1086,7 @@ let create_input_tab filename =
 	    ~name:"processed" 
 	    [`BACKGROUND "light green" ;`EDITABLE false]);
   tv1
-  
+ 
 let main files = 
   let w = GWindow.window 
 	    ~allow_grow:true ~allow_shrink:true 
@@ -1345,7 +1353,10 @@ let main files =
   (* Edit Menu *)
   let edit_menu = factory#add_submenu "_Edit" in
   let edit_f = new GMenu.factory edit_menu ~accel_group in
-  ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._z ~callback:
+  ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback:
+	   (fun () -> 
+	      ignore (get_current_view()).view#undo));
+  ignore(edit_f#add_item "_Clear Undo Stack" ~key:GdkKeysyms._exclam ~callback:
 	   (fun () -> 
 	      ignore (get_current_view()).view#undo));
   ignore(edit_f#add_separator ());
@@ -1372,6 +1383,8 @@ let main files =
 				   (out_some v.analyzed_view)#set_read_only b
 				) 
   in
+  read_only_i#misc#set_state `INSENSITIVE;
+
   to_do_on_page_switch := 
   (fun i -> 
      prerr_endline ("Switching to tab "^(string_of_int i));
@@ -1519,14 +1532,15 @@ let main files =
   add_complex_template 
     ("_Inductive __", "Inductive ident : :=\n  | : .\n",
      14, 5, Some GdkKeysyms._I);
-  let add_simple_template (menu_text, text) =
-    ignore (templates_factory#add_item menu_text
+  let add_simple_template (factory: GMenu.menu GMenu.factory) 
+(menu_text, text) =
+    ignore (factory#add_item menu_text
 	    ~callback:(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 
+  List.iter (add_simple_template templates_factory)
     [ "_Auto", "Auto ";
       "_Auto with *", "Auto with * ";
       "_EAuto", "EAuto ";
@@ -1539,13 +1553,38 @@ let main files =
     ];
   ignore (templates_factory#add_separator ());
   List.iter 
-    (fun s -> add_simple_template ("_"^s, s^" ")) 
+    (fun l -> 
+       match l with 
+	 |[s] -> add_simple_template templates_factory ("_"^s, s^" ") 
+	 | [] -> ()
+	 | s::r -> 
+	     let a = "_@..." in
+	     a.[1] <- s.[0];
+	     let f = templates_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.commands;
   
   (* Commands Menu *)
   let commands_menu =  factory#add_submenu "_Commands" in
   let commands_factory = new GMenu.factory commands_menu ~accel_group in
-
+  
+  (* Command/Show commands *)
+  let commands_show_m = commands_factory#add_item 
+			  "_Show commands" 
+			  ~callback:(Command_windows.command_window ())
+			  #window#present
+  in  
+  
   (* Command/Compile Menu *)
   let compile_f () =
     let v = get_active_view () in
@@ -1578,7 +1617,8 @@ let main files =
     !flash_info 
       (current.cmd_coqmakefile ^ if c = 0 then " succeeded" else " failed")
   in
-  let _ = commands_factory#add_item "_Make Makefile" ~callback:coq_makefile_f in
+  let _ = commands_factory#add_item "_Make Makefile" ~callback:coq_makefile_f 
+  in
 
   (* Configuration Menu *)
   let reset_revert_timer () =
@@ -1628,16 +1668,17 @@ let main files =
 	    ~callback:(fun () -> browse current.library_url) in
   let _ = 
     help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1
-      ~callback:(fun () ->
-		   let av = out_some ((get_current_view ()).analyzed_view) in 
-		   match GtkBase.Clipboard.wait_for_text (cb ()) with
-		     | None -> 
-			 prerr_endline "None selected";
-			 av#help_for_keyword ()
-		     | Some t ->
- 			 prerr_endline "Some selected";
-			 prerr_endline t;
-			 browse_keyword t)
+      ~callback:(fun () -> 
+  let av = out_some ((get_current_view ()).analyzed_view) in 
+		 av#help_for_keyword ())
+  in
+  let _ = 
+    help_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2
+      ~callback:(fun () -> let term = get_current_word () in
+		(Command_windows.command_window ())#new_command
+		 ~command:"SearchAbout"
+		  ~term 
+		  ())
   in
   let _ = help_factory#add_separator () in
   let about_m = help_factory#add_item "_About" in
@@ -1788,12 +1829,15 @@ let start () =
      GtkMain.Rc.add_default_file (Filename.concat (Sys.getenv "HOME") ".coqiderc");
   with Not_found -> ());
   ignore (GtkMain.Main.init ());
+  GtkData.AccelGroup.set_default_mod_mask 
+    (Some [`CONTROL;`SHIFT;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5;`LOCK]);
   cb_ := Some (GtkBase.Clipboard.get Gdk.Atom.primary);
   Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
 						      `WARNING;`CRITICAL]
     (fun ~level msg ->
          failwith ("Coqide internal error: " ^ msg)
     );
+  Command_windows.main ();
   main files;
   Sys.catch_break true;
   while true do 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 784c4a4d4..20a06ae12 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -106,3 +106,14 @@ let set_highlight_timer f =
 	revert_timer := 
 	Some (GMain.Timeout.add ~ms:2000 
 		~callback:(fun () -> f (); highlight_timer := None; true))
+
+
+(* Get back the standard coq out channels *)
+let read_stdout,clear_stdout =
+  let out_buff = Buffer.create 100 in
+  Pp_control.std_ft := Format.formatter_of_buffer out_buff;
+  (fun () -> Format.pp_print_flush !Pp_control.std_ft (); 
+     let r = Buffer.contents out_buff in
+     Buffer.clear out_buff; r),
+  (fun () -> 
+     Format.pp_print_flush !Pp_control.std_ft (); Buffer.clear out_buff)
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 23aed3c07..398d0ef59 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -126,7 +126,7 @@ let (current:pref) =
     automatic_tactics = [];
     
     modifier_for_navigation = [`CONTROL; `MOD1];
-    modifier_for_templates = [`SHIFT; `CONTROL];
+    modifier_for_templates = [`MOD4];
     
     cmd_browse = "netscape -remote \"OpenURL(", ")\"";
 
diff --git a/ide/undo.ml b/ide/undo.ml
index c05902236..1b74926cb 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -4,12 +4,17 @@ type action =
   | Insert of string * int * int (* content*pos*length *) 
   | Delete of string * int * int (* content*pos*length *) 
 
+let neg act = match act with
+  | Insert (s,i,l) -> Delete (s,i,l)
+  | Delete (s,i,l) -> Insert (s,i,l)
+
 class undoable_view (tv:Gtk.textview Gtk.obj) =
   let undo_lock = ref true in 
 object(self)
   inherit GText.view tv as super
   val history = (Stack.create () : action Stack.t)
   val redo = (Queue.create () : action Queue.t)
+  val nredo = (Stack.create () : action Stack.t)
 
   method private dump_debug =
     if !debug then begin
@@ -36,6 +41,7 @@ object(self)
 
     end
 
+  method clear_undo = Stack.clear history
   method undo = if !undo_lock then begin
     undo_lock := false;
     prerr_endline "UNDO";
@@ -54,7 +60,9 @@ object(self)
 	      (Stack.push act history; false)
       in if r then begin
 	process_pending ();
-	Queue.push (Stack.pop history) redo
+	let act = Stack.pop history in
+	Queue.push act redo;
+	Stack.push act nredo
       end;
       undo_lock := true; 
       r
@@ -71,6 +79,8 @@ object(self)
 	      ~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;
@@ -101,7 +111,6 @@ 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,
diff --git a/ide/undo.mli b/ide/undo.mli
index 36700f396..0aae49e79 100644
--- a/ide/undo.mli
+++ b/ide/undo.mli
@@ -5,6 +5,7 @@ object
   inherit GText.view
   method undo : bool
   method redo : bool
+  method clear_undo : unit
 end
 
 val undoable_view :