diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2012-10-02 12:26:51 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2012-10-02 12:26:51 +0000 |
commit | cec38cb9a73e4731f0ff220faa6f9286e4226c83 (patch) | |
tree | 9338a949370388594e0506c88ebcff7c191981a7 /coq/coq.el | |
parent | 45d0afbce4c193abf47219628e85a03abe1a11d0 (diff) |
Fixed 'as' close automatic insertion.
Diffstat (limited to 'coq/coq.el')
-rw-r--r-- | coq/coq.el | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -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 () |