diff options
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r-- | generic/proof-script.el | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 19cebe9c..a3f4a52c 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1889,14 +1889,23 @@ try to avoid duplicating them in the buffer. When used in the locked region (and so with strict read only off), it always defaults to inserting a semi (nicer might be to parse for a comment, and insert or skip to the next semi)." - (let ((mrk (point)) ins incomment) + (let ((mrk (point)) + (termregexp (regexp-quote proof-terminal-string)) + ins incomment nwsp) (if (< mrk (proof-unprocessed-begin)) (insert proof-terminal-string) ; insert immediately in locked region (if (proof-only-whitespace-to-locked-region-p) (error "There's nothing to do!")) (skip-chars-backward " \t\n") + (setq nwsp (point)) ; char after first non-whitespace (unless (or proof-electric-terminator-noterminator - (looking-at (regexp-quote proof-terminal-string))) + ;; before the terminal + (looking-at termregexp) + ;; after the terminal + (and + (re-search-backward termregexp (proof-unprocessed-begin)) + (goto-char nwsp) + (eq (match-end 0) nwsp))) (insert proof-terminal-string) (setq ins t)) (let* ((pos |