diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-01-31 18:19:48 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-01-31 18:19:48 +0000 |
| commit | c02f5a7215698872dd38f6b7e06d3943b1067824 (patch) | |
| tree | f5f3882962893f21306237d4a6217f31c0a760fb | |
| parent | cf6f0face58b8cdd4b280e7101381a8175823027 (diff) | |
Fix problem noticed with Isar and repeated comments.
| -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 fc2e618b..01bc9f7b 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1614,11 +1614,20 @@ This version is used when `proof-script-command-start-regexp' is set." ;; (If it were accepted it could upset the ;; undo behaviour) (goto-char prev-no-blanks) + ;; Update: PG 3.4: try to deal with sequences + ;; of comments as well, since previous behaviour + ;; breaks Isar, in fact, since repeated + ;; comments get categorized as commands, + ;; breaking sync. (if (and (looking-at commentre) (re-search-forward proof-comment-end-regexp) - (skip-chars-forward " \t\n") - (>= (point) comend)) + (progn + (skip-chars-forward " \t\n") + (while (looking-at commentre) + (skip-chars-forward " \t\n") + (re-search-forward proof-comment-end-regexp)) + (>= (point) comend))) 'comment 'cmd))) (string (if (eq type 'comment) "" bufstr))) (setq prev (point)) |