From 87af89b6acfaf48afc3166f10371bf6d190241f0 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 8 Mar 2005 16:41:51 +0000 Subject: making holes.el cleaner, with the help of Stefan Monnier. I had to adapt coq.el to these modifications. --- coq/coq-abbrev.el | 2 +- coq/coq.el | 12 +++--------- 2 files changed, 4 insertions(+), 10 deletions(-) (limited to 'coq') diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index d2e31539..29fc9b96 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -221,7 +221,7 @@ ["fun3 f3" (holes-insert-and-expand "f3") t] ["fun4 f4" (holes-insert-and-expand "f4") t] "" - ["if then else if" (holes-insert-and-expand "li") t] + ["if then else if" (holes-insert-and-expand "if") t] ["let in li" (holes-insert-and-expand "li") t] "" ["match m" (holes-insert-and-expand "m") t] diff --git a/coq/coq.el b/coq/coq.el index d034ff92..cbc5a056 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -106,7 +106,7 @@ 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 ".") - (holes-replace-string-by-holes-backward-move-point 1 holes-empty-hole-string) + (holes-replace-string-by-holes-backward p) (goto-char p) (holes-set-point-next-hole-destroy)) ) @@ -128,10 +128,10 @@ To disable coqc being called (and use only make), set this to nil." (if (string-equal typkind "") (progn (insert mods " " s ".\n#\nEnd " s ".") - (holes-replace-string-by-holes-backward-move-point 1 holes-empty-hole-string) + (holes-replace-string-by-holes-backward p) (goto-char p)) (insert mods " " s " " typkind " #.\n#\nEnd " s ".") - (holes-replace-string-by-holes-backward-move-point 2 holes-empty-hole-string) + (holes-replace-string-by-holes-backward p) (goto-char p) (holes-set-point-next-hole-destroy)) ) @@ -639,12 +639,6 @@ Based on idea mentioned in Coq reference manual." ;; mode: you can use this (C-c C-l) to do what binding below did. ;;(define-key coq-keymap [(control f3)] 'coq-three-b) -; This is arguable, but completion with a three key shortcut is bad, -; and the default meta-/ is bad on some keyboards (especially french ones) -(define-key global-map [(control backspace)] 'expand-abbrev) -;; da: do you also want a key for unexpand-abbrev? (maybe just undo is ok) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Indentation ;; -- cgit v1.2.3