From c02f5a7215698872dd38f6b7e06d3943b1067824 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 31 Jan 2002 18:19:48 +0000
Subject: Fix problem noticed with Isar and repeated comments.

---
 generic/proof-script.el | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'generic')

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))
-- 
cgit v1.2.3