aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-06-09 12:30:09 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-06-09 12:30:09 +0000
commitbe7a95a0f2165895aa1d0fd8b0edb3633da00fcc (patch)
tree5ac95427b6001d3a56d183ede327e8e201273ff6
parentdd77dbe4696d5d39728bb47ef351877d286d8782 (diff)
Fix compile errors (seems to be code duplication between coq.el and coq-indent)
-rw-r--r--coq/coq-indent.el11
-rw-r--r--coq/coq.el13
2 files changed, 12 insertions, 12 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index d5f3b49d..8892b696 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -234,6 +234,17 @@ and return nil."
(looking-at "{\\|\\."))) 1)
(t 0)))
+(defun coq-empty-command-p ()
+ "Test if between point and previous command is empty.
+Comments are ignored, of course."
+ (let ((end (point))
+ (start (coq-find-not-in-comment-backward "[^[:space:]]")))
+ ;; we must find a "." to be sure, because {O} {P} is allowed in definitions
+ ;; with implicits --> this function is recursive
+ (if (looking-at "{\\|}") (coq-empty-command-p)
+ (looking-at "\\."))))
+
+
; slight modification of proof-script-generic-parse-cmdend (one of the
; candidate for proof-script-parse-function), to allow "{" and "}" to be
; command terminator when the command is empty. TO PLUG: swith the comment
diff --git a/coq/coq.el b/coq/coq.el
index f6821cc5..a51da38b 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -465,22 +465,11 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
;;;;;;;;;;; purpose.
; coq-end-command-regexp is ni coq-indent.el
-(setq coq-script-command-end-regexp coq-end-command-regexp)
+(defconst coq-script-command-end-regexp coq-end-command-regexp)
; "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)")
-(defun coq-empty-command-p ()
- "Test if between point and previous command is empty.
-Comments are ignored, of course."
- (let ((end (point))
- (start (coq-find-not-in-comment-backward "[^[:space:]]")))
- ;; we must find a "." to be sure, because {O} {P} is allowed in definitions
- ;; with implicits --> this function is recursive
- (if (looking-at "{\\|}") (coq-empty-command-p)
- (looking-at "\\."))))
-
-
; slight modification of proof-script-generic-parse-cmdend (one of the
; candidate for proof-script-parse-function), to allow "{" and "}" to be
; command terminator when the command is empty. TO PLUG: swith the comment