aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2012-10-03 21:22:56 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2012-10-03 21:22:56 +0000
commitc92764731e963e84226eb623af7aa3be576fb5ce (patch)
treeb0d63df1c535417350be367bdf58867798a94df4 /coq
parent09a7c8f5bf7e080c8853895a26b212a11f4163a4 (diff)
"as" insertion on a region.
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el15
1 files changed, 13 insertions, 2 deletions
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)
+ )
+ ))