IDE: menu templates

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

4 files changed, 364 insertions, 30 deletions

diff --git a/Makefile b/Makefile
index a790eb4fa0..3060360931 100644
--- a/Makefile
+++ b/Makefile
@@ -446,7 +446,8 @@ COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.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/find_phrase.cmo \
-          ide/highlight.cmo ide/coq.cmo ide/coqide.cmo
+          ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \
+	  ide/coq_tactics.cmo ide/coqide.cmo
 
 COQIDECMX=$(COQIDECMO:.cmo=.cmx)
 COQIDEFLAGS=-I +lablgtk2
@@ -455,7 +456,7 @@ beforedepend:: ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml
 FULLIDELIB=$(FULLCOQLIB)/ide
 IDEFILES=ide/coq.png ide/.coqiderc
 
-ide: $(COQIDE) states
+ide: $(COQIDEBYTE) $(COQIDE) states
 
 $(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQIDECMX)
 	$(COQMKTOP) -ide -opt $(COQIDEFLAGS) lablgtk.cmxa $(OPTFLAGS) -o $@ $(COQIDECMX)
@@ -923,7 +924,16 @@ install-opt:
 
 install-binaries:
 	$(MKDIR) $(FULLBINDIR)
-	cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(COQINTERFACE) $(COQVO2XML) $(COQIDE) $(FULLBINDIR)
+	cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(COQINTERFACE) $(COQVO2XML) $(FULLBINDIR)
+
+install-ide: install-ide-$(BEST)
+	cd $(FULLBINDIR); ln -sf coqide.$(BEST)$(EXE) coqide$(EXE)
+
+install-ide-byte:
+	cp $(COQIDEBYTE) $(FULLBINDIR)
+
+install-ide-opt: install-ide-byte
+	cp $(COQIDEOPT) $(FULLBINDIR)
 
 LIBFILES=$(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO)
 LIBFILESLIGHT=$(INITVO) $(THEORIESLIGHTVO)
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
new file mode 100644
index 0000000000..773fe54f6b
--- /dev/null
+++ b/ide/coq_commands.ml
@@ -0,0 +1,182 @@
+let commands = [
+  "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 Rec LoadPath";
+  "Add Rec ML Path";
+  "Add Ring";
+  "Add Semi Ring";
+  "Add Semi Ring";
+  "Add Setoid";
+  "Axiom";
+  "Back";
+  "Begin Silent";
+  "Canonical Structure";
+  "Cd";
+  "Chapter";
+  "Check";
+  "Coercion";
+  "Coercion Local";
+  "CoFixpoint";
+  "CoInductive";
+  "Correctness";
+  "Declare ML Module";
+  "Defined";
+  "Definition";
+  "Derive Dependent Inversion";
+  "Derive Dependent Inversion_clear";
+  "Derive Inversion";
+  "Derive Inversion_clear";
+  "Drop";
+  "End";
+  "End Silent";
+  "Eval";
+  "Explicitation of implicit arguments";
+  "Extract Constant";
+  "Extract Inductive";
+  "Extraction";
+  "Extraction Inline";
+  "Extraction Language";
+  "Extraction Module";
+  "Extraction NoInline";
+  "Fact";
+  "Fixpoint";
+  "Focus";
+  "Global Variable";
+  "Goal";
+  "Grammar";
+  "Hint;
+    * Hint Constructors";
+  "Hint Unfold";
+  "Hint";
+  "Hint Rewrite";
+  "Hints Extern";
+  "Hints Immediate";
+  "Hints Resolve";
+  "Hints Immediate";
+  "Hints Resolve";
+  "Hints Unfold";
+  "Hypothesis";
+  "Identity Coercion";
+  "Implicit Arguments Off";
+  "Implicit Arguments On";
+  "Implicits";
+  "Inductive";
+  "Infix";
+  "Inspect";
+  "Lemma";
+  "Load";
+  "Load Verbose";
+  "Local";
+  "Locate";
+  "Locate File";
+  "Locate Library";
+  "Module";
+  "Module Type";
+  "Mutual Inductive";
+  "Notation";
+  "Opaque";
+  "Parameter";
+  "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";
+  "Proof";
+  "Pwd";
+  "Qed";
+  "Quit";
+  "Read Module";
+  "Record";
+  "Recursive Extraction";
+  "Recursive Extraction Module";
+  "Remark";
+  "Remove LoadPath";
+  "Remove Printing If ident";
+  "Remove Printing Let ident";
+  "Require";
+  "Require Export";
+  "Reset";
+  "Reset Extraction Inline";
+  "Reset Initial";
+  "Restart";
+  "Restore State";
+  "Resume";
+  "Save";
+  "Scheme";
+  "Search";
+  "Search ... inside ...";
+  "Search ... outside ...";
+  "SearchAbout";
+  "SearchPattern";
+  "SearchPattern ... inside ...";
+  "SearchPattern ... outside ...";
+  "SearchRewrite";
+  "SearchRewrite ... inside ...";
+  "SearchRewrite ... outside ...";
+  "Section";
+  "Set Extraction AutoInline";
+  "Set Extraction Optimize";
+  "Set Hyps_limit";
+  "Set Implicit Arguments";
+  "Set Printing Coercion";
+  "Set Printing Coercions";
+  "Set Printing Synth";
+  "Set Printing Wildcard";
+  "Set Undo";
+  "Show";
+  "Show Conjectures";
+  "Show Implicits";
+  "Show Intro";
+  "Show Intros";
+  "Show Programs";
+  "Show Proof";
+  "Show Script";
+  "Show Tree";
+  "Structure";
+  "Suspend";
+  "Syntactic Definition";
+  "Syntax";
+  "Tactic Definition";
+  "Test Printing If ident";
+  "Test Printing Let ident";
+  "Test Printing Synth";
+  "Test Printing Wildcard";
+  "Theorem";
+  "Time";
+  "Transparent";
+  "Undo";
+  "Unfocus";
+  "Unset Extraction AutoInline";
+  "Unset Extraction Optimize";
+  "Unset Hyps_limit";
+  "Unset Implicit Arguments";
+  "Unset Printing Coercion";
+  "Unset Printing Coercions";
+  "Unset Printing Synth";
+  "Unset Printing Wildcard";
+  "Unset Undo";
+  "Variable";
+  "Variables";
+  "Write State";
+]
diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml
new file mode 100644
index 0000000000..7cac14da4b
--- /dev/null
+++ b/ide/coq_tactics.ml
@@ -0,0 +1,124 @@
+let tactics = [
+  "Abstract";
+  "Absurd";
+  "Apply";
+  "Apply ... with";
+  "Assert";
+  "Assumption";
+  "Auto";
+  "AutoRewrite";
+  "Binding list";
+  "Case";
+  "Case ... with";
+  "Cbv";
+  "Change";
+  "Change ... in";
+  "Clear";
+  "ClearBody";
+  "Compare";
+  "Compute";
+  "Constructor";
+  "Constructor ... with";
+  "Contradiction";
+  "Conversion tactics";
+  "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 <-";
+  "Derive Inversion";
+  "Destruct";
+  "Discriminate";
+  "DiscrR";
+  "Do";
+  "Double Induction";
+  "EApply";
+  "EAuto";
+  "Elim ... using";
+  "Elim ... with";
+  "ElimType";
+  "Exact";
+  "Exists";
+  "Fail";
+  "Field";
+  "First";
+  "Fold";
+  "Fourier";
+  "Generalize";
+  "Generalize Dependent";
+  "Print Hint";
+  "Hnf";
+  "Idtac";
+  "Induction";
+  "Info";
+  "Injection";
+  "Intro";
+  "Intro ... after";
+  "Intro after";
+  "Intros";
+  "Intros pattern";
+  "Intros until";
+  "Intuition";
+  "Inversion";
+  "Inversion ... in";
+  "Inversion ... using";
+  "Inversion ... using ... in";
+  "Inversion_clear";
+  "Inversion_clear ... in";
+  "LApply";
+  "Lazy";
+  "Left";
+  "LetTac";
+  "Move";
+  "NewDestruct";
+  "NewInduction";
+  "Omega";
+  "Orelse";
+  "Pattern";
+  "Pose";
+  "Prolog";
+  "Quote";
+  "Red";
+  "Refine";
+  "Reflexivity";
+  "Rename";
+  "Repeat";
+  "Replace ... with";
+  "Rewrite";
+  "Rewrite ->";
+  "Rewrite -> ... in";
+  "Rewrite <-";
+  "Rewrite <- ... in";
+  "Rewrite ... in";
+  "Right";
+  "Ring";
+  "Setoid_replace";
+  "Setoid_rewrite";
+  "Simpl";
+  "Simple Inversion";
+  "Simplify_eq";
+  "Solve";
+  "Split";
+  "SplitAbsolu";
+  "SplitRmult";
+  "Subst";
+  "Symmetry";
+  "Tacticals";
+  "Tauto";
+  "Transitivity";
+  "Trivial";
+  "Try";
+  "tactic macros";
+  "Unfold";
+  "Unfold ... in";
+]
+
+
+
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 250a521b72..3cf0a911fc 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1446,7 +1446,7 @@ let main files =
 	    ~callback:(do_if_active (fun a -> a#insert_command "Progress Simpl.\n" "Simpl.\n" ))
 	 );
   ignore (tactics_factory#add_item "Tauto"
-	    ~key:GdkKeysyms._t
+	    ~key:GdkKeysyms._p
 	    ~callback:(do_if_active (fun a -> a#insert_command "Tauto.\n" "Tauto.\n" ))
 	 );
   ignore (tactics_factory#add_item "Trivial"
@@ -1467,42 +1467,60 @@ let main files =
 	 );
   
   (* Templates Menu *)
-  let templates_menu =  factory#add_submenu "Templates" in
+  let templates_menu =  factory#add_submenu "_Templates" in
   let templates_factory = new GMenu.factory templates_menu 
 			    ~accel_group 
 			    ~accel_modi:current.modifier_for_templates
   in
-  let templates_tactics = templates_factory#add_submenu "Tactics" in
-  let templates_tactics_factory = new GMenu.factory templates_tactics ~accel_group in
-  ignore (templates_tactics_factory#add_item "Auto");
-  ignore (templates_tactics_factory#add_item "Auto with *");
-  ignore (templates_tactics_factory#add_item "EAuto");
-  ignore (templates_tactics_factory#add_item "EAuto with *");
-  ignore (templates_tactics_factory#add_item "Intuition");
-  ignore (templates_tactics_factory#add_item "Omega");
-  ignore (templates_tactics_factory#add_item "Simpl");
-  ignore (templates_tactics_factory#add_item "Tauto");
-  ignore (templates_tactics_factory#add_item "Trivial");
-  let templates_commands = templates_factory#add_submenu "Commands" in
-  let templates_commands_factory = new GMenu.factory templates_commands 
-				     ~accel_group 
-				     ~accel_modi:[`MOD1]
-  in
-  (* Templates/Commands/Lemma *)
-  let callback () = 
-    let {view = view } = get_current_view () in
-    if (view#buffer#insert_interactive "Lemma new_lemma : .\nProof.\n\nSave.\n") then
-      begin
+  let add_complex_template (menu_text, text, offset, len, key) =
+  (* Templates/Lemma *)
+    let callback () = 
+      let {view = view } = get_current_view () in
+      if view#buffer#insert_interactive text then begin
 	let iter = view#buffer#get_iter_at_mark `INSERT in
-	ignore (iter#nocopy#backward_chars 19);
+	ignore (iter#nocopy#backward_chars offset);
 	view#buffer#move_mark `INSERT iter;
-	ignore (iter#nocopy#backward_chars 9);
+	ignore (iter#nocopy#backward_chars len);
 	view#buffer#move_mark `SEL_BOUND iter;
 	Highlight.highlight_all view#buffer
       end
+    in
+    ignore (templates_factory#add_item menu_text ~callback ?key)
   in
-  ignore (templates_commands_factory#add_item "Lemma _" ~callback ~key:GdkKeysyms._L);
-
+  add_complex_template 
+    ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n", 
+     19, 9, Some GdkKeysyms._L);
+  add_complex_template 
+    ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n", 
+     19, 11, Some GdkKeysyms._L);
+  add_complex_template 
+    ("_Definition __", "Definition ident := .\n",
+     6, 5, Some GdkKeysyms._D);
+  add_complex_template 
+    ("_Inductive __", "Inductive ident : :=\n  | : .\n",
+     14, 5, Some GdkKeysyms._N);
+  let add_simple_template (menu_text, text) =
+    ignore (templates_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 
+    [ "_Auto", "Auto ";
+      "Auto with _*", "Auto with * ";
+      "_EAuto", "EAuto ";
+      "EA_uto with *", "EAuto with * ";
+      "_Intuition", "Intuition ";
+      "_Omega", "Omega ";
+      "_Simpl", "Simpl ";
+      "_Tauto", "Tauto ";
+      "Tri_vial", "Trivial ";
+    ];
+  ignore (templates_factory#add_separator ());
+  List.iter 
+    (fun s -> add_simple_template ("_"^s, s^" ")) 
+    Coq_commands.commands;
   
   (* Commands Menu *)
   let commands_menu =  factory#add_submenu "Commands" in