diff options
| author | David Aspinall | 2004-04-06 16:11:46 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-04-06 16:11:46 +0000 |
| commit | d985cda3b7142b09b84e9daad67c8d2f82e59495 (patch) | |
| tree | 1a29a5cd684f895de37e6040d27c627bf27be4ab /generic | |
| parent | f2a08e7eca05aeea848711626ccb073d9508b605 (diff) | |
Adjust proof-script-comment-end to fix comment-end to be empty for end-of-line comments.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 13 | ||||
| -rw-r--r-- | generic/proof-script.el | 12 |
2 files changed, 18 insertions, 7 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 0d08f89e..0450d8f2 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -888,11 +888,11 @@ initial ``goal'' and the final ``save'' command." :group 'prover-config) (defcustom proof-script-fly-past-comments nil - "*If non-nil, fly past comments when scripting, coalescing them into single spans. + "*If non-nil, fly past successive comments when scripting, coalescing into single spans. The default setting for this before PG 3.5 was t, now it is nil. If you prefered the old behaviour, customize this variable to t." :type 'boolean - :group 'prover-config) + :group 'proof-user-options) (defcustom proof-script-parse-function nil "A function which parses a portion of the proof script. @@ -931,12 +931,15 @@ but you can set this variable to something else more precise if necessary." :type 'string :group 'proof-script) -(defcustom proof-script-comment-end "\n" +(defcustom proof-script-comment-end "" "String which ends a comment in the proof assistant command language. -The script buffer's comment-end is set to a space plus this string. +Should be an empty string if comments are terminated by end-of-line +The script buffer's comment-end is set to a space plus this string, +if it is non-empty. + See also `proof-script-comment-start'. -You should set this variable for reliable working of Proof General," +You should set this variable for reliable working of Proof General." :type 'string :group 'proof-script) diff --git a/generic/proof-script.el b/generic/proof-script.el index 7ee34569..0d14f43f 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2527,12 +2527,20 @@ assistant." (make-local-variable 'comment-start) (setq comment-start (concat proof-script-comment-start " ")) (make-local-variable 'comment-end) - (setq comment-end (concat " " proof-script-comment-end)) + (setq comment-end + ;; For end of line terminated comments, stays empty. + (if (string-equal "" proof-script-comment-end) + "" + ;; Otherwise, an extra space before comment delimiter + (concat " " proof-script-comment-end))) (unless proof-script-comment-start-regexp (setq proof-script-comment-start-regexp (regexp-quote proof-script-comment-start))) (unless proof-script-comment-end-regexp - (setq proof-script-comment-end-regexp (regexp-quote proof-script-comment-end))) + (setq proof-script-comment-end-regexp + (if (string-equal "" proof-script-comment-end) + (regexp-quote "\n") ;; end-of-line terminated comments + (regexp-quote proof-script-comment-end)))) (make-local-variable 'comment-start-skip) (setq comment-start-skip |