From 40d0c079ac9acf8ddd1e531b6e229ccd71451bd4 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 13 Mar 2015 14:12:13 +0000 Subject: (fixes last commit) Added a command to send Queries to coq, with completion (C-c C-a C-q). Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag. --- lib/holes.el | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/lib/holes.el b/lib/holes.el index 7bceeb8b..09eb9dde 100644 --- a/lib/holes.el +++ b/lib/holes.el @@ -613,9 +613,11 @@ created. Return the number of holes created." -(defun holes-replace-string-by-holes-backward-jump (pos &optional noindent) +(defun holes-replace-string-by-holes-backward-jump (pos &optional noindent alwaysjump) "Put holes between POS and point, backward, indenting. -\"#\" and \"@{..}\" between this positions will become holes." +\"#\" and \"@{..}\" between this positions will become holes. If +ALWAYSJUMP is non nil, jump to the first hole even if more than +one." (unless noindent (save-excursion (indent-region pos (point) nil))) (let ((n (holes-replace-string-by-holes-backward pos))) (case n @@ -625,6 +627,7 @@ created. Return the number of holes created." (holes-set-point-next-hole-destroy)) ; if only one hole, go to it. (t (goto-char pos) + (when alwaysjump (holes-set-point-next-hole-destroy)) (unless (active-minibuffer-window) ; otherwise minibuffer gets hidden (message (substitute-command-keys "\\[holes-set-point-next-hole-destroy] to jump to active hole. \\[holes-short-doc] to see holes doc."))))))) -- cgit v1.2.3