From cec38cb9a73e4731f0ff220faa6f9286e4226c83 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 2 Oct 2012 12:26:51 +0000 Subject: Fixed 'as' close automatic insertion. --- coq/coq.el | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'coq') diff --git a/coq/coq.el b/coq/coq.el index 059f6d6e..2070efa4 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2392,9 +2392,11 @@ Based on idea mentioned in Coq reference manual. ;goals, it is not detected as a response message. proof-shell-last-output)) (substr (match-string 1 proof-shell-last-output))) ; idem - (coq-script-parse-cmdend-backward) - (let ((inhibit-read-only t)) - (insert (concat " as [" substr "]"))))) + (unless (= (length substr) 0) + (save-excursion + (coq-script-parse-cmdend-backward) + (let ((inhibit-read-only t)) + (insert (concat " as [" substr "]"))))))) (defun coq-insert-match () -- cgit v1.2.3