diff options
| author | Makarius Wenzel | 1999-11-10 14:20:00 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-11-10 14:20:00 +0000 |
| commit | 8423337a5cf175abcb3f9cca77ed49b3b79e1caa (patch) | |
| tree | 726f90aaaab92ca2396b72ffa87a5fc1ae33bb00 /generic | |
| parent | 24c86f6ce52b633973e12457c6ec8c7133209dc7 (diff) | |
fixed indentation bug: use proof-looking-at (proof-case-fold-search);
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-indent.el | 16 | ||||
| -rw-r--r-- | generic/proof-script.el | 8 |
2 files changed, 12 insertions, 12 deletions
diff --git a/generic/proof-indent.el b/generic/proof-indent.el index 0295a3e6..6849cdd6 100644 --- a/generic/proof-indent.el +++ b/generic/proof-indent.el @@ -44,31 +44,31 @@ (setq forward-amount 1) ; may be subject to dynamic scoping! (cond ;; strings - ((and instring (looking-at proof-string-end-regexp)) + ((and instring (proof-looking-at proof-string-end-regexp)) (setq forward-amount (length (match-string 0))) (setq instring nil)) (instring) - ((looking-at proof-string-start-regexp) + ((proof-looking-at proof-string-start-regexp) (setq forward-amount (length (match-string 0))) (setq instring t)) ;; comments - ((looking-at cmt-start-regexp) + ((proof-looking-at cmt-start-regexp) (setq forward-amount (length (match-string 0))) (incf cmt-level)) - ((looking-at cmt-end-regexp) + ((proof-looking-at cmt-end-regexp) (setq forward-amount (length (match-string 0))) (decf cmt-level)) ((> cmt-level 0)) ;; parentheses - ((looking-at "\\s(") + ((proof-looking-at "\\s(") (setq stack (cons (list c (point)) stack))) - ((looking-at "\\s)") + ((proof-looking-at "\\s)") (setq stack (cdr stack))) ;; basic indentation for commands - ((looking-at proof-indent-commands-regexp) + ((proof-looking-at proof-indent-commands-regexp) (setq stack (cons (list proof-terminal-char (point)) stack))) ((and (eq c proof-terminal-char) (eq (car (car stack)) proof-terminal-char)) @@ -128,4 +128,4 @@ (setq state (proof-parse-to-point beg state) beg (point)))))) -(provide 'proof-indent)
\ No newline at end of file +(provide 'proof-indent) diff --git a/generic/proof-script.el b/generic/proof-script.el index 576656df..e0471d5d 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1143,7 +1143,7 @@ the next command end." (setq done t alist (cons 'unclosed-comment alist)))) (setq done t)) ;; Case 3. Found a comment end, not inside a string - ((and (looking-at comment-end-regexp) quote-parity) + ((and (proof-looking-at comment-end-regexp) quote-parity) (if (= depth 0) (progn (message "Warning: extraneous comment end") @@ -1155,7 +1155,7 @@ the next command end." (aset str i ?\ ) (incf i)))) ;; Case 4. Found a comment start, not inside a string - ((and (looking-at comment-start-regexp) quote-parity) + ((and (proof-looking-at comment-start-regexp) quote-parity) (setq depth (+ depth 1)) (forward-char (length (match-string 0)))) ;; Case 5. Inside a comment. @@ -1173,9 +1173,9 @@ the next command end." ;; Maintain quote-parity (cond - ((and quote-parity (looking-at proof-string-start-regexp)) + ((and quote-parity (proof-looking-at proof-string-start-regexp)) (setq quote-parity nil)) - ((and (not quote-parity) (looking-at proof-string-end-regexp)) + ((and (not quote-parity) (proof-looking-at proof-string-end-regexp)) (setq quote-parity t))) (forward-char) |