diff options
| author | David Aspinall | 2002-08-30 09:42:11 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-08-30 09:42:11 +0000 |
| commit | 4bd424dc4e077d0ffc9446d0f58c4a3dcea6f14a (patch) | |
| tree | 3df9215d2038b6fca2acdabf98c6c4412684268c | |
| parent | 4c1ac4904b1c63574dddc5a49458b0960a7255c3 (diff) | |
Patch from Stefan Monnier for using nested-comment aware parser on GNU Emacs.
| -rw-r--r-- | generic/proof-script.el | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 7c1c9f44..0443cd37 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1577,7 +1577,7 @@ to the function which parses the script segment by segment." (setq prevtype type))))) ;; Return segment list segs))) - + (defun proof-script-generic-parse-find-comment-end () "Find the end of the comment point is at the start of. Nil if not found." (let ((notout t)) @@ -1823,10 +1823,14 @@ This version is used when `proof-script-command-end-regexp' is set." ;; (FIXME: ignore nested comments here, we should ;; have a consistent policy!) (unless + (if (fboundp 'comment-forward) + (progn + (goto-char (or (match-end 1) (match-beginning 0))) + (comment-forward)) (proof-re-search-forward - proof-script-comment-end-regexp cmdend t) + proof-script-comment-end-regexp cmdend t)) (error - "PG error: proof-segment-up-to-cmd-end didn't find comment end.")) + "PG error: proof-segment-up-to-cmd-end didn't find comment end")) (setq alist (cons (list 'comment "" (point)) alist))) ;; There should be something left: a command. (skip-chars-forward " \t\n") |