diff options
| author | Pierre Courtieu | 2012-06-09 12:58:56 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2012-06-09 12:58:56 +0000 |
| commit | a65f4b532fe1611aaecb19334ac5cc6671d83b9f (patch) | |
| tree | 0775ac90169c512418dfd799833ed9e9baac78ba | |
| parent | 43493a243f3099e38c39a52cafa801aa4d716a94 (diff) | |
Made a small change in generic code about the setting of
comment-start-skip: if it is already set then proof-script should not
change it. Ultimately if David approves we should moreover fix the
setting itself which is bugged.
coq-mode now sets this variable by itself.
| -rw-r--r-- | coq/coq.el | 5 | ||||
| -rw-r--r-- | generic/proof-script.el | 10 |
2 files changed, 11 insertions, 4 deletions
@@ -1271,6 +1271,11 @@ This is specific to `coq-mode'." (setq proof-script-parse-function 'coq-script-parse-function) (setq proof-script-comment-start "(*") (setq proof-script-comment-end "*)") + (make-local-variable 'comment-start-skip) + (setq comment-start-skip + (if (string-equal "" proof-script-comment-start) + (regexp-quote "\n") ;; end-of-line terminated comments + (regexp-quote proof-script-comment-start))) (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name (setq proof-assistant-home-page coq-www-home-page) diff --git a/generic/proof-script.el b/generic/proof-script.el index 9a9d4042..74e92918 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2390,11 +2390,13 @@ assistant." (regexp-quote "\n") ;; end-of-line terminated comments (regexp-quote proof-script-comment-end)))) + ;; BOGUS (make-local-variable 'comment-start-skip) - (setq comment-start-skip - (if (string-equal "" proof-script-comment-end) - (regexp-quote "\n") ;; end-of-line terminated comments - (regexp-quote proof-script-comment-end)))) + (unless comment-start-skip + (setq comment-start-skip + (if (string-equal "" proof-script-comment-end) + (regexp-quote "\n") ;; end-of-line terminated comments + (regexp-quote proof-script-comment-end))))) |