From c92764731e963e84226eb623af7aa3be576fb5ce Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 3 Oct 2012 21:22:56 +0000 Subject: "as" insertion on a region. --- coq/coq.el | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'coq') diff --git a/coq/coq.el b/coq/coq.el index b9522c8e..5ad22876 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2444,7 +2444,7 @@ Typically after a proof-assert-next-command. ;; smaller/faster but since this message is output ;; *before* resulting goals, it is not detected as ;; a response message. - proof-shell-last-output)) + proof-shell-last-output)) (substr (or (and str (match-string 1 proof-shell-last-output)) "")) ;; emptysubstr = t if substr is empty or contains only spaces and | (emptysubstr (and (string-match "\\(\\s-\\||\\)*" substr) @@ -2462,7 +2462,18 @@ Typically after a proof-assert-next-command. ;; this hook will do nothing until infoH is inserted again. (setq coq-last-input-action nil)) - +;; Trying to propose insertion of "as" for a whole region. But iterating +;; proof-assert-next-command-interactive is probably wrong if some error occur +;; during scripting. +(defun coq-insert-as-in-region (&optional beg end) + (let ((beg (or beg (point-min))) + (end (or end (point-max)))) + (goto-char beg) + (while (< (point) end) + (coq-script-parse-cmdend-forward) + (proof-assert-next-command-interactive) + ) + )) -- cgit v1.2.3