From 2fa9fcd55de6357db6fa521291d253432a298ec8 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 6 Apr 2004 16:25:57 +0000
Subject: Adjust proof-script-comment-end and comment-end to hold empty string
 for end-of-line terminated comments.

---
 generic/proof-script.el | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 0d14f43f..970a7407 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1326,11 +1326,14 @@ With ARG, turn on scripting iff ARG is positive."
   "A subroutine of `proof-done-advancing'."
   ;; Add an element for a new span, which should span
   ;; the text of the comment.
-  ;; FIXME: might be better to use regexps for matching
-  ;; start/end of comments, rather than comment-start-skip
+  ;; FIXME: might be better to use regexps/skip spaces for matching
+  ;; start/end of comments, rather than comment-start and
+  ;; comment-end skip (which assumes comments are nicely formatted).
+  ;; 
   (let ((bodyspan  (make-span
 		    (+ (length comment-start) (span-start span))
-		    (- (span-end span) (length comment-end))))
+		    (- (span-end span) 
+		       (max 1 (length comment-end)))))
 	(id        (proof-next-element-id 'comment)))
     (pg-add-element "comment" id bodyspan)
     (set-span-property span 'id (intern id))
-- 
cgit v1.2.3