diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-09-08 13:30:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-09-08 13:30:56 +0000 |
| commit | 10f195216526bd8fc993527d95b0534c5a4f62c7 (patch) | |
| tree | 1d5d731778cf3dc720279a4197612a978e6d5efd /generic | |
| parent | 1775cd0015fff527c9fe34c21900cfd87838d425 (diff) | |
Fix obscure problem with proof-segment-upto-cmdstart with buggy input.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 289e1c51..ebdfc550 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1205,6 +1205,7 @@ which continues past POS, if any. (NOT IMPLEMENTED IN THIS VERSION). This version is used when `proof-script-command-start-regexp' is set." (save-excursion (let* ((commentre (concat "[ \t\n]*" proof-comment-start-regexp)) + (commentend (concat proof-comment-end-regexp "[ \t\n]*" )) (add-segment-for-cmd ; local function: advances "prev" (lambda () (setq tmp (point)) @@ -1222,9 +1223,32 @@ This version is used when `proof-script-command-start-regexp' is set." (goto-char prev) (skip-chars-forward " \t\n") (point))) - (bufstr (buffer-substring prev-no-blanks (point))) - (type (if (eq (string-match commentre bufstr) 0) - 'comment 'cmd)) + (comend (point)) + (bufstr (buffer-substring prev-no-blanks comend)) + (type (save-excursion + ;; The behaviour here is a bit odd: this + ;; is a half-hearted attempt to strip comments + ;; as we send text to the proof assistant, + ;; but it breaks when we have certain bad + ;; input: (* foo *) blah (* bar *) cmd + ;; We check for the case + ;; of a comment spanning the *whole* + ;; substring, otherwise send the + ;; (defective) text as if it were a + ;; proper command anyway. + ;; This shouldn't cause problems: the + ;; proof assistant is certainly capable + ;; of skipping comments itself, and + ;; the situation should cause an error. + ;; (If it were accepted it could upset the + ;; undo behaviour) + (goto-char prev-no-blanks) + (if (and + (looking-at commentre) + (re-search-forward proof-comment-end-regexp) + (skip-chars-forward " \t\n") + (>= (point) comend)) + 'comment 'cmd))) (string (if (eq type 'comment) "" bufstr))) (setq prev (point)) (goto-char tmp) |