cleaning holes.el. All functions are prefixed with "holes-". Also

modified coq.el and coq-abbrev.el accordingly.

2 files changed, 115 insertions, 115 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 78f9aea6..cef21e06 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -148,146 +148,146 @@
   '(
     ("Insert Command" 
       "COMMAND               ABBREVIATION"
-     ["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]
+     ["Definition            def<C-BS>" (holes-insert-and-expand "def") t]
+     ["Fixpoint              fix<C-BS>" (holes-insert-and-expand "fix") t]
+     ["Lemma                 l<C-BS>" (holes-insert-and-expand "l") 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]
+     ["Inductive             indv<C-BS>" (holes-insert-and-expand "indv") t]
+     ["Inductive1            indv1<C-BS>" (holes-insert-and-expand "indv1") t]
+     ["Inductive2             indv2<C-BS>" (holes-insert-and-expand "indv2") t]
+     ["Inductive3            indv3<C-BS>" (holes-insert-and-expand "indv3") t]
+     ["Inductive4            indv4<C-BS>" (holes-insert-and-expand "indv4") t]
      ""
      ["Section..." coq-insert-section t]
      ""
      ("Modules"
       "COMMAND               ABBREVIATION"
       ["Module (interactive)... " coq-insert-module 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]
+      ["Module                mo<C-BS>" (holes-insert-and-expand "mo") t]
+      ["Module (<:)           mo2<C-BS>" (holes-insert-and-expand "mo") t]
+;      ["Module (interactive)  moi<C-BS>" (holes-insert-and-expand "moi") t]
+;      ["Module (interactive <:) moi2<C-BS>" (holes-insert-and-expand "moi2") t]
+      ["Module Type           mt<C-BS>" (holes-insert-and-expand "mt") t]
+;      ["Module Type (interactive) mti<C-BS>" (holes-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]
+      ["Declare Module        dm<C-BS>" (holes-insert-and-expand "dm") t]
+      ["Declare Module (<:)   dm2<C-BS>" (holes-insert-and-expand "dm") t]
+;      ["Declare Module (inter.) dmi<C-BS>" (holes-insert-and-expand "dmi") t]
+;      ["Declare Module (inter. <:) dmi2<C-BS>" (holes-insert-and-expand "dmi2") t]
       )
      ("Hints"
       "COMMAND               ABBREVIATION"
-      ["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 Rewrite          hrw<C-BS>" (insert-and-expand "hrw") t]
-      ["Hint Extern           he<C-BS>" (insert-and-expand "he") t]
+      ["Hint Constructors     hc<C-BS>" (holes-insert-and-expand "hc") t]
+      ["Hint Immediate        hi<C-BS>" (holes-insert-and-expand "hi") t]
+      ["Hint Resolve          hr<C-BS>" (holes-insert-and-expand "hr") t]
+      ["Hint Rewrite          hrw<C-BS>" (holes-insert-and-expand "hrw") t]
+      ["Hint Extern           he<C-BS>" (holes-insert-and-expand "he") t]
      )
      ("Schemes"
       "COMMAND               ABBREVIATION"
-      ["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]
+      ["Scheme                sc<C-BS>" (holes-insert-and-expand "sc") t]
+      ["Functional Scheme     fs<C-BS>" (holes-insert-and-expand "fs") t]
+      ["Functional Scheme with    fsw<C-BS>" (holes-insert-and-expand "fsw") t]
       )
      ("Notations"
       "COMMAND               ABBREVIATION"
-      ["Infix                           inf<C-BS>" (insert-and-expand "inf") t]     
-      ["Notation (no assoc)             nota<C-BS>" (insert-and-expand "nota") t]     
-      ["Notation (assoc)                notas<C-BS>" (insert-and-expand "notas") t]     
-      ["Notation (no assoc, scope)      notasc<C-BS>" (insert-and-expand "notasc") t]     
-      ["Notation (assoc, scope)         notassc<C-BS>" (insert-and-expand "notassc") t]
+      ["Infix                           inf<C-BS>" (holes-insert-and-expand "inf") t]     
+      ["Notation (no assoc)             nota<C-BS>" (holes-insert-and-expand "nota") t]     
+      ["Notation (assoc)                notas<C-BS>" (holes-insert-and-expand "notas") t]     
+      ["Notation (no assoc, scope)      notasc<C-BS>" (holes-insert-and-expand "notasc") t]     
+      ["Notation (assoc, scope)         notassc<C-BS>" (holes-insert-and-expand "notassc") t]
 		""
-      ["Notation (simple)               nots<C-BS>" (insert-and-expand "nots") t]     
-      ["Notation (simple,local)         notsl<C-BS>" (insert-and-expand "nots") t]     
+      ["Notation (simple)               nots<C-BS>" (holes-insert-and-expand "nots") t]     
+      ["Notation (simple,local)         notsl<C-BS>" (holes-insert-and-expand "nots") t]     
 
       )
      )
 
     ("Insert Term" 
      "FORM           ABBREVIATION"
-     ["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]
+     ["forall        fo<C-BS>"  (holes-insert-and-expand "fo") t]
+     ["forall1       fo1<C-BS>"  (holes-insert-and-expand "fo1") t]
+     ["forall2       fo2<C-BS>" (holes-insert-and-expand "fo2") t]
+     ["forall3       fo3<C-BS>" (holes-insert-and-expand "fo3") t]
+     ["forall4       fo4<C-BS>" (holes-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<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]
+     ["fun           f<ctrl-bacspace>"  (holes-insert-and-expand "f") t]
+     ["fun1          f1<ctrl-bacspace>"  (holes-insert-and-expand "f1") t]
+     ["fun2          f2<C-BS>" (holes-insert-and-expand "f2") t]
+     ["fun3          f3<C-BS>" (holes-insert-and-expand "f3") t]
+     ["fun4          f4<C-BS>" (holes-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]
+     ["if then else  if<C-BS>"  (holes-insert-and-expand "li") t]
+     ["let in        li<C-BS>"  (holes-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]
+     ["match         m<C-BS>"  (holes-insert-and-expand "m") t]
+     ["match2        m2<C-BS>"  (holes-insert-and-expand "m2") t]
+     ["match3        m3<C-BS>"  (holes-insert-and-expand "m3") t]
+     ["match4        m4<C-BS>"  (holes-insert-and-expand "m4") t]
      )
 
     ("Insert Tactic (a-f)" 
      "TACTIC           ABBREVIATION"
-     ["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]
+     ["absurd                 abs<C-BS>"  (holes-insert-and-expand "abs") t]
+     ["assumption              as<C-BS>"  (holes-insert-and-expand "as") t]
+     ["assert                 ass<C-BS>"  (holes-insert-and-expand "ass") t]
+     ["auto                     a<C-BS>"  (holes-insert-and-expand "a") t]
+     ["auto with               aw<C-BS>"  (holes-insert-and-expand "aw") t]
+     ["auto with arith        awa<C-BS>"  (holes-insert-and-expand "awa") t]
+     ["autorewrite             ar<C-BS>"  (holes-insert-and-expand "ar") t]
+     ["cases                    c<C-BS>"  (holes-insert-and-expand "c") t]
+     ["change                  ch<C-BS>"  (holes-insert-and-expand "ch") t]
+     ["change in              chi<C-BS>"  (holes-insert-and-expand "chi") t]
+     ["change with in        chwi<C-BS>"  (holes-insert-and-expand "chwi") t]
+     ["constructor            con<C-BS>"  (holes-insert-and-expand "con") t]
+     ["congruence            cong<C-BS>"  (holes-insert-and-expand "cong") t]
+     ["decompose              dec<C-BS>"  (holes-insert-and-expand "dec") t]
+     ["decide equality        deg<C-BS>"  (holes-insert-and-expand "deg") t]
+     ["destruct               des<C-BS>"  (holes-insert-and-expand "des") t]
+     ["destruct using        desu<C-BS>"  (holes-insert-and-expand "desu") t]
+     ["destruct as           desa<C-BS>"  (holes-insert-and-expand "desa") t]
+     ["discriminate           dis<C-BS>"  (holes-insert-and-expand "dis") t]
+     ["eauto                   ea<C-BS>"  (holes-insert-and-expand "ea") t]
+     ["eauto with             eaw<C-BS>"  (holes-insert-and-expand "dec") t]
+     ["elim                     e<C-BS>"  (holes-insert-and-expand "e") t]
+     ["elim using             elu<C-BS>"  (holes-insert-and-expand "elu") t]
+     ["exists                  ex<C-BS>"  (holes-insert-and-expand "ex") t]
+     ["field                  fld<C-BS>"  (holes-insert-and-expand "fld") t]
+     ["firstorder            fsto<C-BS>"  (holes-insert-and-expand "fsto") t]
+     ["fourier                fou<C-BS>"  (holes-insert-and-expand "fou") t]
+     ["functional induction    fi<C-BS>"  (holes-insert-and-expand "fi") t]
      )
 
     ("Insert Tactic (g-z)" 
      "TACTIC           ABBREVIATION"
-     ["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 "ri") t]
-     ["rewrite <-             r<<C-BS>"  (insert-and-expand "rl") t]
-     ["rewrite <- in          ri<<C-BS>"  (insert-and-expand "ril") 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]
+     ["generalize             g<C-BS>"  (holes-insert-and-expand "g") t]
+     ["induction              ind<C-BS>"  (holes-insert-and-expand "ind") t]
+     ["injection              inj<C-BS>"  (holes-insert-and-expand "inj") t]
+     ["intro                  i<C-BS>"  (holes-insert-and-expand "i") t]
+     ["intros                 is<C-BS>"  (holes-insert-and-expand "is") t]
+     ["intuition              intu<C-BS>"  (holes-insert-and-expand "intu") t]
+     ["inversion              inv<C-BS>"  (holes-insert-and-expand "inv") t]
+     ["omega                  om<C-BS>"  (holes-insert-and-expand "om") t]
+     ["pose                   po<C-BS>"  (holes-insert-and-expand "om") t]
+     ["reflexivity            refl<C-BS>"  (holes-insert-and-expand "refl") t]
+     ["replace                rep<C-BS>"  (holes-insert-and-expand "rep") t]
+     ["rewrite                r<C-BS>"  (holes-insert-and-expand "r") t]
+     ["rewrite in             ri<C-BS>"  (holes-insert-and-expand "ri") t]
+     ["rewrite <-             r<<C-BS>"  (holes-insert-and-expand "rl") t]
+     ["rewrite <- in          ri<<C-BS>"  (holes-insert-and-expand "ril") t]
+     ["set                    set<C-BS>"  (holes-insert-and-expand "set") t]
+     ["set in hyp             seth<C-BS>"  (holes-insert-and-expand "seth") t]
+     ["set in goal            setg<C-BS>"  (holes-insert-and-expand "setg") t]
+     ["set in                 seti<C-BS>"  (holes-insert-and-expand "seti") t]
+     ["simpl                  s<C-BS>"  (holes-insert-and-expand "s") t]
+     ["simpl                  si<C-BS>"  (holes-insert-and-expand "si") t]
+     ["split                  sp<C-BS>"  (holes-insert-and-expand "sp") t]
+     ["subst                  su<C-BS>"  (holes-insert-and-expand "su") t]
+     ["symmetry               sym<C-BS>"  (holes-insert-and-expand "sym") t]
+     ["transitivity           trans<C-BS>"  (holes-insert-and-expand "trans") t]
+     ["trivial                t<C-BS>"  (holes-insert-and-expand "t") t]
+     ["tauto                  ta<C-BS>"  (holes-insert-and-expand "ta") t]
+     ["unfold                 u<C-BS>"  (holes-insert-and-expand "u") t]
      )
     ;; da: I added Show sub menu, not sure if it's helpful, but why not.
     ;; FIXME: submenus should be split off here.  Also, these commands
@@ -307,11 +307,11 @@
      ;; "Make a hole active   click on it"
      ;; "Disable a hole   click on it (button 2)"
      ;; "Destroy a hole   click on it (button 3)"
-     ["Make hole at point"  set-make-active-hole t]
-     ["Make selection a hole"  set-make-active-hole t]
-     ["Replace active hole by selection"  replace-update-active-hole t]
-     ["Jump to active hole"  set-point-next-hole-destroy t]
-     ["Forget all holes in buffer"  clear-all-buffer-holes t]
+     ["Make hole at point"  holes-set-make-active-hole t]
+     ["Make selection a hole"  holes-set-make-active-hole t]
+     ["Replace active hole by selection"  holes-replace-update-active-hole t]
+     ["Jump to active hole"  holes-set-point-next-hole-destroy t]
+     ["Forget all holes in buffer"  holes-clear-all-buffer-holes t]
      ["Tell me about holes?" holes-short-doc t]
      ;; look a bit better at the bottom
      "Make hole with mouse: C-M-select"
diff --git a/coq/coq.el b/coq/coq.el
index 1d10a246..fcd6a753 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -106,9 +106,9 @@ To disable coqc being called (and use only make), set this to nil."
   (interactive  "sSection name: ")
   (let ((p (point)))
     (insert "Section " s ".\n#\nEnd " s ".")
-    (replace-string-by-holes-backward-move-point 1 empty-hole-string)
+    (holes-replace-string-by-holes-backward-move-point 1 holes-empty-hole-string)
     (goto-char p)
-    (set-point-next-hole-destroy))
+    (holes-set-point-next-hole-destroy))
 )
 
 (defconst module-kinds-table 
@@ -128,12 +128,12 @@ To disable coqc being called (and use only make), set this to nil."
     (if (string-equal typkind "")
         (progn
           (insert mods " " s ".\n#\nEnd " s ".")
-          (replace-string-by-holes-backward-move-point 1 empty-hole-string)
+          (holes-replace-string-by-holes-backward-move-point 1 holes-empty-hole-string)
           (goto-char p))
       (insert mods " " s " " typkind " #.\n#\nEnd " s ".")
-      (replace-string-by-holes-backward-move-point 2 empty-hole-string)
+      (holes-replace-string-by-holes-backward-move-point 2 holes-empty-hole-string)
       (goto-char p)
-      (set-point-next-hole-destroy))
+      (holes-set-point-next-hole-destroy))
     )
   )
 ;  (completing-read "Section name: " )