added submenus for command insertion for coq. menu uses abbrev

expansion to build holes.

3 files changed, 209 insertions, 127 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index baad752c..dbcaac92 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -7,170 +7,176 @@
 (if (boundp 'holes-abbrev-complete)
 	 (define-abbrev-table 'coq-mode-abbrev-table
 		'(
-		  ("u" "unfold" nil 0)
-		  ("si" "simpl" nil 0)
-		  ("t" "trivial" nil 0)
-		  ("dec" "decompose []" nil 0)
+		  ("a" "auto" nil 0)
 		  ("ab" "absurd" nil 0)
+		  ("abs" "absurd" nil 0)
 		  ("ao" "abstract omega" nil 0)
-		  ("s" "simpl" nil 0)
-		  ("r<" "rewrite <-" nil 0)
-		  ("r" "rewrite" nil 0)
-		  ("di" "discriminate" nil 0)
-		  ("p" "Print" nil 0)
-		  ("indv" "Inductive" nil 0)
-		  ("o" "abstract omega" nil 0)
-		  ("l" "Lemma  :" nil 0)
+		  ("ap" "apply" nil 0)
+		  ("as" "assumption" nil 0)
+		  ("au" "auto" nil 0)
+		  ("aw" "auto with" nil 0)
 		  ("awa" "auto with arith" nil 0)
-		  ("i" "intro" nil 0)
-		  ("h" "Hints  : ." nil 0)
-		  ("g" "generalize" nil 0)
 		  ("con" "constructor" nil 0)
+		  ("dec" "decompose []" nil 0)
+		  ("def" "Definition : :=." nil 0)
+		  ("di" "discriminate" nil 0)
+		  ("dis" "discriminate" nil 0)
 		  ("e" "elim" nil 0)
-		  ("ge" "generalize" nil 0)
-		  ("sym" "symmetry" nil 0)
-		  ("a" "auto" nil 0)
-		  ("re" "rewrite" nil 0)
-		  ("eawa" "eauto with arith" nil 0)
-		  ("un" "unfold" nil 0)
+		  ("ea" "eauto" nil 0)
+		  ("eap" "eapply" nil 0)
 		  ("eaw" "eauto with" nil 0)
+		  ("eawa" "eauto with arith" nil 0)
+		  ("el" "elim" nil 0)
+		  ("ex" "exists" nil 0)
 		  ("f" "forall #:#,#" nil 0)
+		  ("f" "fun (:) => " nil 0)
 		  ("fi" "functional induction" nil 0)
+		  ("fix" "Fixpoint X (X : X) {struct X} : X := X." nil 0)
 		  ("fs" "Functional Scheme xxx := Induction for yyy (opt:with ...)." nil 0)
-		  ("sc" "Scheme := Induction for Sort ." nil 0)
-		  ("f" "fun (:) => " nil 0)
-		  ("eap" "eapply" nil 0)
-		  ("ex" "exists" nil 0)
-		  ("inv" "inversion" nil 0)
-		  ("is" "intros" nil 0)
-		  ("abs" "absurd" nil 0)
-		  ("tr" "trivial" nil 0)
-		  ("in" "intro" nil 0)
-		  ("dis" "discriminate" nil 0)
-		  ("aw" "auto with" nil 0)
-		  ("pr" "Print" nil 0)
-		  ("au" "auto" nil 0)
-		  ("as" "assumption" nil 0)
-		  ("sy" "symmetry" nil 0)
-		  ("el" "elim" nil 0)
-		  ("ap" "apply" nil 0)
+		  ("g" "generalize" nil 0)
+		  ("ge" "generalize" nil 0)
 		  ("gen" "generalize" nil 0)
+		  ("h" "Hints  : ." nil 0)
 		  ("hr" "Hint Resolve :." nil 0)
+		  ("i" "intro" nil 0)
+		  ("in" "intro" nil 0)
 		  ("ind" "induction" nil 0)
-		  ("fix" "Fixpoint X (X : X) {struct X} : X := X." nil 0)
+		  ("indv" "Inductive" nil 0)
+		  ("inv" "inversion" nil 0)
+		  ("is" "intros" nil 0)
+		  ("l" "Lemma  :" nil 0)
+		  ("o" "abstract omega" nil 0)
+		  ("p" "Print" nil 0)
+		  ("pr" "Print" nil 0)
+		  ("r" "rewrite" nil 0)
+		  ("r<" "rewrite <-" nil 0)
+		  ("re" "rewrite" nil 0)
 		  ("re<" "rewrite <-" nil 0)
-		  ("ea" "eauto" nil 0)
-		  ("def" "Definition : :=." nil 0)
+		  ("s" "simpl" nil 0)
+		  ("sc" "Scheme := Induction for Sort ." nil 0)
+		  ("si" "simpl" nil 0)
+		  ("sy" "symmetry" nil 0)
+		  ("sym" "symmetry" nil 0)
+		  ("t" "trivial" nil 0)
+		  ("tr" "trivial" nil 0)
+		  ("u" "unfold" nil 0)
+		  ("un" "unfold" nil 0)
 		  ))
   (define-abbrev-table 'coq-mode-abbrev-table
 	 '(
+		("a" "auto" holes-abbrev-complete 4)
+		("ab" "absurd #" holes-abbrev-complete 0)
+		("abs" "absurd #" holes-abbrev-complete 0)
+		("ap" "apply #" holes-abbrev-complete 16)
+		("as" "assumption" holes-abbrev-complete 4)
+		("au" "auto" holes-abbrev-complete 1)
+		("aw" "auto with #" holes-abbrev-complete 1)
+		("awa" "auto with arith" holes-abbrev-complete 4)
+		("c" "cases #" holes-abbrev-complete 1)
+		("con" "constructor" holes-abbrev-complete 3)
+		("dec" "decompose [#] #" holes-abbrev-complete 3)
+		("def" "Definition #:# := #." holes-abbrev-complete 5)
+		("def2" "Definition # (# : #) (# : #):# := #." holes-abbrev-complete 5)
+		("def3" "Definition # (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
+		("def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
+		("di" "discriminate" holes-abbrev-complete 0)
+		("dis" "discriminate" holes-abbrev-complete 0)
+		("e" "elim #" holes-abbrev-complete 1)
+		("ea" "eauto" holes-abbrev-complete 0)
+		("eap" "eapply #" holes-abbrev-complete 0)
+		("eaw" "eauto with #" holes-abbrev-complete 0)
+		("eawa" "eauto with arith" holes-abbrev-complete 0)
+		("el" "elim #" holes-abbrev-complete 0)
+		("elu" "elim # using #" holes-abbrev-complete 0)
+		("ex" "exists #" holes-abbrev-complete 0)
+		("f" "fun # => #" holes-abbrev-complete 0)
+		("f1" "fun #:# => #" holes-abbrev-complete 0)
+		("f2" "fun (#:#) (#:#) => #" holes-abbrev-complete 0)
+		("f3" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
+		("f4" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
+		("fi" "functional induction #" holes-abbrev-complete 0)
+		("fix" "Fixpoint # (#:#) {struct #} : # :=" holes-abbrev-complete 3)
+		("fo" "forall #,#" holes-abbrev-complete 0)
+		("fo1" "forall #:#,#" holes-abbrev-complete 0)
+		("fo2" "forall (#:#) (#:#), #" holes-abbrev-complete 0)
+		("fo3" "forall (#:#) (#:#) (#:#), #" holes-abbrev-complete 0)
+		("fo4" "forall (#:#) (#:#) (#:#) (#:#), #" holes-abbrev-complete 0)
+		("fs" "Functional Scheme # := Induction for #." holes-abbrev-complete 0)
+		("fsw" "Functional Scheme # := Induction for # with #." holes-abbrev-complete 0)
+		("g" "generalize #" holes-abbrev-complete 0)
+		("ge" "generalize #" holes-abbrev-complete 0)
+		("gen" "generalize #" holes-abbrev-complete 0)
+		("he" "Hint # : # := Extern # # #." holes-abbrev-complete 0)
+		("hi" "Hint Immediate #: #." holes-abbrev-complete 0)
+		("hr" "Hint Resolve #: #." holes-abbrev-complete 0)
+		("hs" "Hints # : #." holes-abbrev-complete 0)
+		("hu" "Hint Unfold #: #." holes-abbrev-complete 0)
+		("i" "intro #" holes-abbrev-complete 10)
+		("if" "if # then # else #" holes-abbrev-complete 1)
+		("in" "intro" holes-abbrev-complete 1)
+		("ind" "induction #" holes-abbrev-complete 2)
+		("indv" "Inductive # : # := # : #." holes-abbrev-complete 0)
+		("inv" "inversion #" holes-abbrev-complete 9)
+		("is" "intros #" holes-abbrev-complete 11)
+		("ite" "if # then # else #" holes-abbrev-complete 1)
+		("l" "Lemma # : #." holes-abbrev-complete 4)
+		("li" "let # := # in #" holes-abbrev-complete 1)
+		("o" "omega" holes-abbrev-complete 0)
+		("om" "Omega" holes-abbrev-complete 0)
+		("p" "Print #" holes-abbrev-complete 3)
+		("pr" "print #" holes-abbrev-complete 2)
+		("r" "rewrite #" holes-abbrev-complete 19)
+		("r<" "rewrite <- #" holes-abbrev-complete 0)
+		("re" "rewrite #" holes-abbrev-complete 0)
+		("re<" "rewrite <- #" holes-abbrev-complete 0)
+		("s" "simpl" holes-abbrev-complete 23)
+		("sc" "Scheme # := Induction for # Sort #." nil 0)
+		("si" "simpl" holes-abbrev-complete 0)
+		("sp" "Split" holes-abbrev-complete 1)
+		("sy" "symmetry" holes-abbrev-complete 0)
+		("sym" "symmetry" holes-abbrev-complete 0)
+		("t" "trivial" holes-abbrev-complete 1)
+		("tr" "trivial" holes-abbrev-complete 7)
+		("u" "unfold #" holes-abbrev-complete 1)
+		("un" "unfold #" holes-abbrev-complete 7)
 		("m" "match # with 
 # => #" holes-abbrev-complete 1)
-		("m|" "match # with 
+		("m2" "match # with 
  # => #
 | # => #" holes-abbrev-complete 1)
-		("m||" "match # with 
+		("m3" "match # with 
   # => #
 | # => #
 | # => #" holes-abbrev-complete 1)
-		("m|||" "match # with 
+		("m4" "match # with 
   # => #
 | # => #
 | # => #
 | # => #" holes-abbrev-complete 1)
-		("m||||" "match # with 
+		("m5" "match # with 
   # => #
 | # => #
 | # => #
 | # => #
 | # => #" holes-abbrev-complete 1)
-		("c" "cases #" holes-abbrev-complete 1)
-		("u" "unfold #" holes-abbrev-complete 1)
-		("si" "simpl" holes-abbrev-complete 0)
-		("t" "trivial" holes-abbrev-complete 1)
-		("dec" "decompose [#] #" holes-abbrev-complete 3)
-		("ab" "absurd #" holes-abbrev-complete 0)
-		("om" "abstract Omega" holes-abbrev-complete 0)
-		("s" "simpl" holes-abbrev-complete 23)
-		("r<" "rewrite <- #" holes-abbrev-complete 0)
-		("r" "rewrite #" holes-abbrev-complete 19)
-		("di" "discriminate" holes-abbrev-complete 0)
-		("p" "Print #" holes-abbrev-complete 3)
-		("indv" "Inductive # : # := #." holes-abbrev-complete 0)
-		("indv|" "Inductive # : # :=
+		("indv2" "Inductive # : # :=
   # : #
 | # : #." holes-abbrev-complete 0)
-		("indv||" "Inductive # : # :=
+		("indv3" "Inductive # : # :=
   # : #
 | # : #
 | # : #." holes-abbrev-complete 0)
-		("indv|||" "Inductive # : # :=
+		("indv4" "Inductive # : # :=
   # : #
 | # : #
 | # : #
 | # : #." holes-abbrev-complete 0)
-		("indv||||" "Inductive # : # :=
+		("indv5" "Inductive # : # :=
   # : #
 | # : #
 | # : #
 | # : #
 | # : #." holes-abbrev-complete 0)
-		("o" "abstract omega" holes-abbrev-complete 0)
-		("l" "Lemma # : #." holes-abbrev-complete 4)
-		("awa" "auto with arith" holes-abbrev-complete 4)
-		("i" "intro #" holes-abbrev-complete 10)
-		("h" "Hints # : #." holes-abbrev-complete 0)
-		("g" "generalize #" holes-abbrev-complete 0)
-		("fo" "forall #,#" holes-abbrev-complete 0)
-		("fo:" "forall #:#,#" holes-abbrev-complete 0)
-		("fo::" "forall (#:#) (#:#), #" holes-abbrev-complete 0)
-		("fo:::" "forall (#:#) (#:#) (#:#), #" holes-abbrev-complete 0)
-		("fo::::" "forall (#:#) (#:#) (#:#) (#:#), #" holes-abbrev-complete 0)
-		("f" "fun # => #" holes-abbrev-complete 0)
-		("f:" "fun #:# => #" holes-abbrev-complete 0)
-		("f::" "fun (#:#) (#:#) => #" holes-abbrev-complete 0)
-		("f:::" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
-		("f::::" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
-		("e" "elim #" holes-abbrev-complete 1)
-		("con" "constructor" holes-abbrev-complete 3)
-		("ge" "generalize #" holes-abbrev-complete 0)
-		("sym" "symmetry" holes-abbrev-complete 0)
-		("a" "auto" holes-abbrev-complete 4)
-		("re" "rewrite #" holes-abbrev-complete 0)
-		("eawa" "eauto with arith" holes-abbrev-complete 0)
-		("un" "unfold #" holes-abbrev-complete 7)
-		("eaw" "eauto with #" holes-abbrev-complete 0)
-		("fi" "functional induction #" holes-abbrev-complete 0)
-		("fs" "Functional Scheme # := Induction for #." 
-		 holes-abbrev-complete 0)
-		("fsw" "Functional Scheme # := Induction for # with #." 
-		 holes-abbrev-complete 0)
-		("sc" "Scheme # := Induction for # Sort #." nil 0)
-		("eap" "eapply #" holes-abbrev-complete 0)
-		("ex" "exists #" holes-abbrev-complete 0)
-		("inv" "inversion #" holes-abbrev-complete 9)
-		("is" "intros #" holes-abbrev-complete 11)
-		("abs" "absurd #" holes-abbrev-complete 0)
-		("tr" "trivial" holes-abbrev-complete 7)
-		("in" "intro" holes-abbrev-complete 1)
-		("dis" "discriminate" holes-abbrev-complete 0)
-		("aw" "auto with #" holes-abbrev-complete 1)
-		("pr" "print #" holes-abbrev-complete 2)
-		("au" "auto" holes-abbrev-complete 1)
-		("as" "assumption" holes-abbrev-complete 4)
-		("sy" "symmetry" holes-abbrev-complete 0)
-		("el" "elim #" holes-abbrev-complete 0)
-		("ap" "apply #" holes-abbrev-complete 16)
-		("gen" "generalize #" holes-abbrev-complete 0)
-		("hr" "Hint Resolve : #." holes-abbrev-complete 0)
-		("ind" "induction #" holes-abbrev-complete 2)
-		("fix" "Fixpoint # (#:#) {struct #} : # :=" holes-abbrev-complete 3)
-		("re<" "rewrite <- #" holes-abbrev-complete 0)
-		("ea" "eauto" holes-abbrev-complete 0)
-		("def" "Definition #:# := #." holes-abbrev-complete 5)
-		("def2" "Definition # (# : #) (# : #):# := #." holes-abbrev-complete 5)
-		("def3" "Definition # (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
-		("def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
 		)
 	 )
   )
diff --git a/coq/coq.el b/coq/coq.el
index 804db615..b36f1dc0 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -86,22 +86,92 @@
 ;; ----- coq specific menu
 
 (defpgdefault menu-entries
-  '(["Print..." coq-Print t]
+  '(
+    ("Insert Command" 
+      "COMMAND               ABBREVIATION"
+     ["Definition            def<ctrl-backspace>" (insert-and-expand "def") t]
+     ["Fixpoint              fix<ctrl-backspace>" (insert-and-expand "fix") t]
+     ["Functional Scheme     fs<ctrl-backspace>" (insert-and-expand "fs") t]
+     ["Functional Scheme w   fs<ctrl-backspace>" (insert-and-expand "fs") t]
+     ["Inductive             indv<ctrl-backspace>" (insert-and-expand "indv") t]
+     ["Inductive1            indv1<ctrl-backspace>" (insert-and-expand "indv1") t]
+     ["Inductive2             indv2<ctrl-backspace>" (insert-and-expand "indv2") t]
+     ["Inductive3            indv3<ctrl-backspace>" (insert-and-expand "indv3") t]
+     ["Inductive4            indv4<ctrl-backspace>" (insert-and-expand "indv4") t]
+     ["Lemma                 l<ctrl-backspace>" (insert-and-expand "l") t]
+     ["Scheme                sc<ctrl-backspace>" (insert-and-expand "sc") t]
+     ["hint Immediate        hi<ctrl-backspace>" (insert-and-expand "hi") t]
+     ["hint Resolve          hr<ctrl-backspace>" (insert-and-expand "hr") t]
+     ["hint extern           he<ctrl-backspace>" (insert-and-expand "he") t]
+     ["hints                 hs<ctrl-backspace>" (insert-and-expand "hs") t]
+     )
+
+    ("Insert term" 
+     "FORM           ABBREVIATION"
+     ["forall        fo<ctrl-backspace>"  (insert-and-expand "fo") t]
+     ["forall1       fo1<ctrl-backspace>"  (insert-and-expand "fo1") t]
+     ["forall2       fo2<ctrl-backspace>" (insert-and-expand "fo2") t]
+     ["forall3       fo3<ctrl-backspace>" (insert-and-expand "fo3") t]
+     ["forall4       fo4<ctrl-backspace>" (insert-and-expand "fo4") t]
+     ["fun           f<ctrl-bacspace>"  (insert-and-expand "f") t]
+     ["fun1          f1<ctrl-bacspace>"  (insert-and-expand "f1") t]
+     ["fun2          f2<ctrl-backspace>" (insert-and-expand "f2") t]
+     ["fun3          f3<ctrl-backspace>" (insert-and-expand "f3") t]
+     ["fun4          f4<ctrl-backspace>" (insert-and-expand "f4") t]
+     ["if then else  if<ctrl-backspace>"  (insert-and-expand "li") t]
+     ["let in        li<ctrl-backspace>"  (insert-and-expand "li") t]
+     ["match         m<ctrl-backspace>"  (insert-and-expand "m") t]
+     ["match2        m2<ctrl-backspace>"  (insert-and-expand "m2") t]
+     ["match3        m3<ctrl-backspace>"  (insert-and-expand "m3") t]
+     ["match4        m4<ctrl-backspace>"  (insert-and-expand "m4") t]
+     ["match5        m5<ctrl-backspace>"  (insert-and-expand "m5") t]
+     )
+
+    ("Insert tactic" 
+     "TACTIC           ABBREVIATION"
+     ["absurd                 ab<ctrl-bacspace>"  (insert-and-expand "ab") t]
+     ["absurd                 abs<ctrl-bacspace>"  (insert-and-expand "abs") t]
+     ["assumption             as<ctrl-bacspace>"  (insert-and-expand "as") t]
+     ["auto                   a<ctrl-bacspace>"  (insert-and-expand "a") t]
+     ["auto with              aw<ctrl-bacspace>"  (insert-and-expand "aw") t]
+     ["auto with arith        awa<ctrl-bacspace>"  (insert-and-expand "awa") t]
+     ["cases                  c<ctrl-bacspace>"  (insert-and-expand "c") t]
+     ["decompose              dec<ctrl-bacspace>"  (insert-and-expand "dec") t]
+     ["discriminate           di<ctrl-bacspace>"  (insert-and-expand "di") t]
+     ["eauto                  ea<ctrl-bacspace>"  (insert-and-expand "ea") t]
+     ["eauto with             eaw<ctrl-bacspace>"  (insert-and-expand "dec") t]
+     ["elim                   e<ctrl-bacspace>"  (insert-and-expand "e") t]
+     ["elim using             elu<ctrl-bacspace>"  (insert-and-expand "elu") t]
+     ["exists                 ex<ctrl-bacspace>"  (insert-and-expand "ex") t]
+     ["functional induction   fi<ctrl-bacspace>"  (insert-and-expand "fi") t]
+     ["generalize             g<ctrl-bacspace>"  (insert-and-expand "g") t]
+     ["induction              ind<ctrl-bacspace>"  (insert-and-expand "ind") t]
+     ["intro                  i<ctrl-bacspace>"  (insert-and-expand "i") t]
+     ["intros                 is<ctrl-bacspace>"  (insert-and-expand "is") t]
+     ["inversion              inv<ctrl-bacspace>"  (insert-and-expand "inv") t]
+     ["omega                  om<ctrl-bacspace>"  (insert-and-expand "om") t]
+     ["rewrite                r<ctrl-bacspace>"  (insert-and-expand "r") t]
+     ["simpl                  s<ctrl-bacspace>"  (insert-and-expand "s") t]
+     ["simpl                  si<ctrl-bacspace>"  (insert-and-expand "si") t]
+     ["split                  sp<ctrl-bacspace>"  (insert-and-expand "sp") t]
+     ["symmetry               sym<ctrl-bacspace>"  (insert-and-expand "sym") t]
+     ["trivial                t<ctrl-bacspace>"  (insert-and-expand "t") t]
+     ["trivial                tr<ctrl-bacspace>"  (insert-and-expand "tr") t]
+     ["unfold                 u<ctrl-bacspace>"  (insert-and-expand "u") t]
+     )
+
+    ["Print..." coq-Print t]
     ["Check..." coq-Check t]
     ["Hints" coq-PrintHint t]
-    ["Intros..." coq-Intros t]
     ["Show ith goal..." coq-Show t]
-    ["Apply"  coq-Apply t]
     ["Search isos/pattern..." coq-SearchIsos t]
     ["expand abbrev at point" expand-abbrev t]
-    ["list abbrevs" list-abbrevs t]
     ["What are those #??" (holes-short-doc) t]
-    ["insert Fixpoint" (insert-and-expand "fix") t]
-    ["insert Definition" (insert-and-expand "def") t]
+    ["list abbrevs" list-abbrevs t]
     ["3 buffers view" coq-three-b t]
     ["Begin Section..." coq-begin-Section t]
     ["End Section" coq-end-Section t]
-    ["Compile" coq-Compile t]))
+    ["Compile" coq-Compile t] ))
 
 
 
diff --git a/generic/holes.el b/generic/holes.el
index ab68925f..aefa519c 100644
--- a/generic/holes.el
+++ b/generic/holes.el
@@ -841,10 +841,16 @@ created"
 	(count-holes-in-last-expand) empty-hole-string)
   )
 
+; insert the expansion of abbrev s, and replace #s by holes. It was
+; possible to implement it with a simple ((insert s) (expand-abbrev))
+; but undo would show the 2 steps, which is bad.
 
 (defun insert-and-expand (s)
-  (insert s)
-  (expand-abbrev)
+  (let* ((exp (abbrev-expansion s))
+		  (c (count-char-in-string empty-hole-string exp)))
+	 (insert exp)
+	 (replace-string-by-holes-backward-move-point c empty-hole-string)
+	 )
   )
 
 (provide 'holes)