diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2011-06-09 12:30:09 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2011-06-09 12:30:09 +0000 |
| commit | be7a95a0f2165895aa1d0fd8b0edb3633da00fcc (patch) | |
| tree | 5ac95427b6001d3a56d183ede327e8e201273ff6 | |
| parent | dd77dbe4696d5d39728bb47ef351877d286d8782 (diff) | |
Fix compile errors (seems to be code duplication between coq.el and coq-indent)
| -rw-r--r-- | coq/coq-indent.el | 11 | ||||
| -rw-r--r-- | coq/coq.el | 13 |
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 @@ -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 |