aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-indent.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2011-09-04 20:58:05 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2011-09-04 20:58:05 +0000
commit43638aa4eed9f78e0e4a59b5bcee5b9896c738bc (patch)
tree817907767e550387fd3919ad1d40ec255618e253 /coq/coq-indent.el
parent6b001acf18f1d931502484a4d85b6820afe91375 (diff)
Fix trac #420 indentation freezing.
Diffstat (limited to 'coq/coq-indent.el')
-rw-r--r--coq/coq-indent.el22
1 files changed, 10 insertions, 12 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 891319d9..f042baef 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -278,7 +278,9 @@ command end regexp."
(goto-char (match-beginning 1))
(not (coq-empty-command-p)))
nil)
- (proof-buffer-syntactic-context)))
+ (and
+ (goto-char foundend)
+ (proof-buffer-syntactic-context))))
;; go back as far as possible before the start of the current
;; matching string, this way we will match consecutive endings
;; like ine "}."
@@ -310,9 +312,9 @@ and return nil."
;; first shift if we are in the middle of a ending pattern
(if (> (coq-is-on-ending-context) 0)
(ignore-errors(forward-char (coq-is-on-ending-context))))
- (let (foundend next-pos)
+ (let (foundbeg next-pos)
;; Find end of command
- (while (and (setq foundend
+ (while (and (setq foundbeg
(and
(re-search-backward proof-script-command-end-regexp limit t)
(match-beginning 1)))
@@ -323,10 +325,12 @@ and return nil."
(goto-char (match-beginning 1))
(not (coq-empty-command-p)))
nil)
- (proof-buffer-syntactic-context)))
+ (and
+ (goto-char foundbeg)
+ (proof-buffer-syntactic-context))))
(ignore-errors (goto-char next-pos)))
- (if (and foundend
- (goto-char foundend) ; move to command end
+ (if (and foundbeg
+ (goto-char foundbeg) ; move to command end
(not (proof-buffer-syntactic-context)))
;; Found command end outside string/comment
'cmd
@@ -384,12 +388,6 @@ Can jump line if NOJUMPLINES = nil."
(setq res (cons command-found res))
(if (and (coq-script-parse-cmdend-forward)
;(ignore-errors (forward-char 1) t);to fit in the "and"
- ;; da: My PATCH for Trac #416, to avoid looping at buffer end
- (not (let ((p (point)))
- (skip-chars-forward " \t\n")
- (prog1
- (eobp)
- (goto-char p))))
(coq-find-real-start))
(setq command-found (coq-command-at-point nojumplines))
(setq command-found nil)