added a menu for hole operations

1 files changed, 109 insertions, 98 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 4bc20706..ce233856 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -91,126 +91,137 @@
   '(
     ("Insert Command" 
       "COMMAND               ABBREVIATION"
-     ["Definition            def<ctrl-backspace>" (insert-and-expand "def") t]
-     ["Fixpoint              fix<ctrl-backspace>" (insert-and-expand "fix") t]
-     ["Lemma                 l<ctrl-backspace>" (insert-and-expand "l") t]
+     ["Definition            def<C-BS>" (insert-and-expand "def") t]
+     ["Fixpoint              fix<C-BS>" (insert-and-expand "fix") t]
+     ["Lemma                 l<C-BS>" (insert-and-expand "l") 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]
+     ["Inductive             indv<C-BS>" (insert-and-expand "indv") t]
+     ["Inductive1            indv1<C-BS>" (insert-and-expand "indv1") t]
+     ["Inductive2             indv2<C-BS>" (insert-and-expand "indv2") t]
+     ["Inductive3            indv3<C-BS>" (insert-and-expand "indv3") t]
+     ["Inductive4            indv4<C-BS>" (insert-and-expand "indv4") t]
      ""
-     ["Module                mo<ctrl-backspace>" (insert-and-expand "mo") t]
-     ["Module (<:)           mo2<ctrl-backspace>" (insert-and-expand "mo") t]
-     ["Module (interactive)  moi<ctrl-backspace>" (insert-and-expand "moi") t]
-     ["Module (interactive <:) moi2<ctrl-backspace>" (insert-and-expand "moi2") t]
-     ["Module Type           mt<ctrl-backspace>" (insert-and-expand "mt") t]
-     ["Module Type (interactive) mti<ctrl-backspace>" (insert-and-expand "mti") t]
-     ["Declare Module        dm<ctrl-backspace>" (insert-and-expand "dm") t]
-     ["Declare Module (<:)   dm2<ctrl-backspace>" (insert-and-expand "dm") t]
-     ["Declare Module (inter.) dmi<ctrl-backspace>" (insert-and-expand "dmi") t]
-     ["Declare Module (inter. <:) dmi2<ctrl-backspace>" (insert-and-expand "dmi2") t]
+     ["Module                mo<C-BS>" (insert-and-expand "mo") t]
+     ["Module (<:)           mo2<C-BS>" (insert-and-expand "mo") t]
+     ["Module (interactive)  moi<C-BS>" (insert-and-expand "moi") t]
+     ["Module (interactive <:) moi2<C-BS>" (insert-and-expand "moi2") t]
+     ["Module Type           mt<C-BS>" (insert-and-expand "mt") t]
+     ["Module Type (interactive) mti<C-BS>" (insert-and-expand "mti") t]
+     ["Declare Module        dm<C-BS>" (insert-and-expand "dm") t]
+     ["Declare Module (<:)   dm2<C-BS>" (insert-and-expand "dm") t]
+     ["Declare Module (inter.) dmi<C-BS>" (insert-and-expand "dmi") t]
+     ["Declare Module (inter. <:) dmi2<C-BS>" (insert-and-expand "dmi2") t]
      ""
-     ["Scheme                sc<ctrl-backspace>" (insert-and-expand "sc") t]
-     ["Functional Scheme     fs<ctrl-backspace>" (insert-and-expand "fs") t]
-     ["Functional Scheme with    fsw<ctrl-backspace>" (insert-and-expand "fsw") t]
+     ["Scheme                sc<C-BS>" (insert-and-expand "sc") t]
+     ["Functional Scheme     fs<C-BS>" (insert-and-expand "fs") t]
+     ["Functional Scheme with    fsw<C-BS>" (insert-and-expand "fsw") t]
      ""
-     ["hint Constructors     hc<ctrl-backspace>" (insert-and-expand "hc") 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]
+     ["hint Constructors     hc<C-BS>" (insert-and-expand "hc") t]
+     ["hint Immediate        hi<C-BS>" (insert-and-expand "hi") t]
+     ["hint Resolve          hr<C-BS>" (insert-and-expand "hr") t]
+     ["hint extern           he<C-BS>" (insert-and-expand "he") t]
+     ["hints                 hs<C-BS>" (insert-and-expand "hs") t]
      ""
-     ["infix                 inf<ctrl-backspace>" (insert-and-expand "inf") t]     
+     ["infix                 inf<C-BS>" (insert-and-expand "inf") 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]
+     ["forall        fo<C-BS>"  (insert-and-expand "fo") t]
+     ["forall1       fo1<C-BS>"  (insert-and-expand "fo1") t]
+     ["forall2       fo2<C-BS>" (insert-and-expand "fo2") t]
+     ["forall3       fo3<C-BS>" (insert-and-expand "fo3") t]
+     ["forall4       fo4<C-BS>" (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]
+     ["fun2          f2<C-BS>" (insert-and-expand "f2") t]
+     ["fun3          f3<C-BS>" (insert-and-expand "f3") t]
+     ["fun4          f4<C-BS>" (insert-and-expand "f4") t]
+     ["if then else  if<C-BS>"  (insert-and-expand "li") t]
+     ["let in        li<C-BS>"  (insert-and-expand "li") t]
+     ["match         m<C-BS>"  (insert-and-expand "m") t]
+     ["match2        m2<C-BS>"  (insert-and-expand "m2") t]
+     ["match3        m3<C-BS>"  (insert-and-expand "m3") t]
+     ["match4        m4<C-BS>"  (insert-and-expand "m4") t]
      )
 
     ("Insert tactic (a-f)" 
      "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]
-     ["assert                 ass<ctrl-bacspace>"  (insert-and-expand "ass") 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]
-     ["autorewrite            ar<ctrl-bacspace>"  (insert-and-expand "ar") t]
-     ["cases                  c<ctrl-bacspace>"  (insert-and-expand "c") t]
-     ["change                 ch<ctrl-bacspace>"  (insert-and-expand "ch") t]
-     ["change in              chi<ctrl-bacspace>"  (insert-and-expand "chi") t]
-     ["change with in         chwi<ctrl-bacspace>"  (insert-and-expand "chwi") t]
-     ["constructor            con<ctrl-bacspace>"  (insert-and-expand "con") t]
-     ["congruence             cong<ctrl-bacspace>"  (insert-and-expand "cong") t]
-     ["decompose              dec<ctrl-bacspace>"  (insert-and-expand "dec") t]
-     ["decide equality        deg<ctrl-bacspace>"  (insert-and-expand "deg") t]
-     ["destruct               des<ctrl-bacspace>"  (insert-and-expand "des") t]
-     ["destruct using         desu<ctrl-bacspace>"  (insert-and-expand "desu") t]
-     ["destruct as            desa<ctrl-bacspace>"  (insert-and-expand "desa") t]
-     ["discriminate           dis<ctrl-bacspace>"  (insert-and-expand "dis") 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]
-     ["field                  fld<ctrl-bacspace>"  (insert-and-expand "fld") t]
-     ["firstorder             fsto<ctrl-bacspace>"  (insert-and-expand "fsto") t]
-     ["fourier                fou<ctrl-bacspace>"  (insert-and-expand "fou") t]
-     ["functional induction   fi<ctrl-bacspace>"  (insert-and-expand "fi") t]
+     ["absurd                 abs<C-BS>"  (insert-and-expand "abs") t]
+     ["assumption              as<C-BS>"  (insert-and-expand "as") t]
+     ["assert                 ass<C-BS>"  (insert-and-expand "ass") t]
+     ["auto                     a<C-BS>"  (insert-and-expand "a") t]
+     ["auto with               aw<C-BS>"  (insert-and-expand "aw") t]
+     ["auto with arith        awa<C-BS>"  (insert-and-expand "awa") t]
+     ["autorewrite             ar<C-BS>"  (insert-and-expand "ar") t]
+     ["cases                    c<C-BS>"  (insert-and-expand "c") t]
+     ["change                  ch<C-BS>"  (insert-and-expand "ch") t]
+     ["change in              chi<C-BS>"  (insert-and-expand "chi") t]
+     ["change with in        chwi<C-BS>"  (insert-and-expand "chwi") t]
+     ["constructor            con<C-BS>"  (insert-and-expand "con") t]
+     ["congruence            cong<C-BS>"  (insert-and-expand "cong") t]
+     ["decompose              dec<C-BS>"  (insert-and-expand "dec") t]
+     ["decide equality        deg<C-BS>"  (insert-and-expand "deg") t]
+     ["destruct               des<C-BS>"  (insert-and-expand "des") t]
+     ["destruct using        desu<C-BS>"  (insert-and-expand "desu") t]
+     ["destruct as           desa<C-BS>"  (insert-and-expand "desa") t]
+     ["discriminate           dis<C-BS>"  (insert-and-expand "dis") t]
+     ["eauto                   ea<C-BS>"  (insert-and-expand "ea") t]
+     ["eauto with             eaw<C-BS>"  (insert-and-expand "dec") t]
+     ["elim                     e<C-BS>"  (insert-and-expand "e") t]
+     ["elim using             elu<C-BS>"  (insert-and-expand "elu") t]
+     ["exists                  ex<C-BS>"  (insert-and-expand "ex") t]
+     ["field                  fld<C-BS>"  (insert-and-expand "fld") t]
+     ["firstorder            fsto<C-BS>"  (insert-and-expand "fsto") t]
+     ["fourier                fou<C-BS>"  (insert-and-expand "fou") t]
+     ["functional induction    fi<C-BS>"  (insert-and-expand "fi") t]
      )
 
     ("Insert tactic (g-z)" 
      "TACTIC           ABBREVIATION"
-     ["generalize             g<ctrl-bacspace>"  (insert-and-expand "g") t]
-     ["induction              ind<ctrl-bacspace>"  (insert-and-expand "ind") t]
-     ["injection              inj<ctrl-bacspace>"  (insert-and-expand "inj") t]
-     ["intro                  i<ctrl-bacspace>"  (insert-and-expand "i") t]
-     ["intros                 is<ctrl-bacspace>"  (insert-and-expand "is") t]
-     ["intuition              intu<ctrl-bacspace>"  (insert-and-expand "intu") t]
-     ["inversion              inv<ctrl-bacspace>"  (insert-and-expand "inv") t]
-     ["omega                  om<ctrl-bacspace>"  (insert-and-expand "om") t]
-     ["pose                   po<ctrl-bacspace>"  (insert-and-expand "om") t]
-     ["reflexivity            refl<ctrl-bacspace>"  (insert-and-expand "refl") t]
-     ["replace                rep<ctrl-bacspace>"  (insert-and-expand "rep") t]
-     ["rewrite                r<ctrl-bacspace>"  (insert-and-expand "r") t]
-     ["rewrite in             ri<ctrl-bacspace>"  (insert-and-expand "r") t]
-     ["rewrite <-             rl<ctrl-bacspace>"  (insert-and-expand "r") t]
-     ["rewrite <- in          ril<ctrl-bacspace>"  (insert-and-expand "r") t]
-     ["set                    set<ctrl-bacspace>"  (insert-and-expand "set") t]
-     ["set in hyp             seth<ctrl-bacspace>"  (insert-and-expand "seth") t]
-     ["set in goal            setg<ctrl-bacspace>"  (insert-and-expand "setg") t]
-     ["set in                 seti<ctrl-bacspace>"  (insert-and-expand "seti") 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]
-     ["subst                  su<ctrl-bacspace>"  (insert-and-expand "su") t]
-     ["symmetry               sym<ctrl-bacspace>"  (insert-and-expand "sym") t]
-     ["transitivity           trans<ctrl-bacspace>"  (insert-and-expand "trans") t]
-     ["trivial                t<ctrl-bacspace>"  (insert-and-expand "t") t]
-     ["tauto                  ta<ctrl-bacspace>"  (insert-and-expand "ta") t]
-     ["unfold                 u<ctrl-bacspace>"  (insert-and-expand "u") t]
+     ["generalize             g<C-BS>"  (insert-and-expand "g") t]
+     ["induction              ind<C-BS>"  (insert-and-expand "ind") t]
+     ["injection              inj<C-BS>"  (insert-and-expand "inj") t]
+     ["intro                  i<C-BS>"  (insert-and-expand "i") t]
+     ["intros                 is<C-BS>"  (insert-and-expand "is") t]
+     ["intuition              intu<C-BS>"  (insert-and-expand "intu") t]
+     ["inversion              inv<C-BS>"  (insert-and-expand "inv") t]
+     ["omega                  om<C-BS>"  (insert-and-expand "om") t]
+     ["pose                   po<C-BS>"  (insert-and-expand "om") t]
+     ["reflexivity            refl<C-BS>"  (insert-and-expand "refl") t]
+     ["replace                rep<C-BS>"  (insert-and-expand "rep") t]
+     ["rewrite                r<C-BS>"  (insert-and-expand "r") t]
+     ["rewrite in             ri<C-BS>"  (insert-and-expand "r") t]
+     ["rewrite <-             rl<C-BS>"  (insert-and-expand "r") t]
+     ["rewrite <- in          ril<C-BS>"  (insert-and-expand "r") t]
+     ["set                    set<C-BS>"  (insert-and-expand "set") t]
+     ["set in hyp             seth<C-BS>"  (insert-and-expand "seth") t]
+     ["set in goal            setg<C-BS>"  (insert-and-expand "setg") t]
+     ["set in                 seti<C-BS>"  (insert-and-expand "seti") t]
+     ["simpl                  s<C-BS>"  (insert-and-expand "s") t]
+     ["simpl                  si<C-BS>"  (insert-and-expand "si") t]
+     ["split                  sp<C-BS>"  (insert-and-expand "sp") t]
+     ["subst                  su<C-BS>"  (insert-and-expand "su") t]
+     ["symmetry               sym<C-BS>"  (insert-and-expand "sym") t]
+     ["transitivity           trans<C-BS>"  (insert-and-expand "trans") t]
+     ["trivial                t<C-BS>"  (insert-and-expand "t") t]
+     ["tauto                  ta<C-BS>"  (insert-and-expand "ta") t]
+     ["unfold                 u<C-BS>"  (insert-and-expand "u") t]
      )
 
     ["What are those #??" (holes-short-doc) t]
+    ("holes" 
+     "make a hole active   click on it"
+     "disable a hole   click on it (button 2)"
+     "destroy a hole   click on it (button 3)"
+     "make a hole with mouse  C-M-select"
+     ["make a hole at point   C-M-h"  (set-make-active-hole) t]
+     ["make selection a hole  C-M-h"  (set-make-active-hole) t]
+     ["replace active hole by selection C-M-y"  (replace-update-active-hole) t]
+     "replace active hole with mouse  C-M-Shift select"
+     ["jump to active hole M-return"  (set-point-next-hole-destroy) t]
+     ["What are those holes?" (holes-short-doc) t]
+     )
     ["expand abbrev at point" expand-abbrev t]
     ["list abbrevs" list-abbrevs t]
     ["Insert Section..." coq-insert-section t]