diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2011-12-16 15:09:04 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2011-12-16 15:09:04 +0000 |
| commit | 9a09cadf8353ae9b788891363394f4937fcbf278 (patch) | |
| tree | 72b684795ed6758b02e08b2e50fbae85381f0d93 /coq/coq-indent.el | |
| parent | 4f14dc14a32e6bcf0c939989109920d6a3d12815 (diff) | |
Adapting coq syntax recognition to the future v8.4 behavior of bullets
(stand-alone commands), which is different of the experiments made
until now in coq/trunk.
Diffstat (limited to 'coq/coq-indent.el')
| -rw-r--r-- | coq/coq-indent.el | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index f042baef..9f4f2041 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -92,7 +92,7 @@ detect if they start something or not." ;; ". " and "... " are command endings, ".. " is not, same as in ;; proof-script-command-end-regexp in coq.el (defconst coq-end-command-regexp - "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\|\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\)\\(?1:}\\)" + "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\|\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\)\\(?1:}\\)\\|\\(?1:-\\)\\|\\(?1:+\\)\\|\\(?1:\\*\\)" ; "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)" "Regexp matching end of a command. There are 3 substrings: * number 1 is the real coq ending string, @@ -243,8 +243,8 @@ Comments are ignored, of course." (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 "\\.")))) + (if (looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p) + (looking-at "\\.\\|\\`")))) ; slight modification of proof-script-generic-parse-cmdend (one of the @@ -273,7 +273,10 @@ command end regexp." (setq next-pos (+ 1 (match-beginning 0))) (or (if (or (string-equal (match-string 1) "}") - (string-equal (match-string 1) "{")) + (string-equal (match-string 1) "{") + (string-equal (match-string 1) "-") + (string-equal (match-string 1) "+") + (string-equal (match-string 1) "*")) (save-excursion (goto-char (match-beginning 1)) (not (coq-empty-command-p))) @@ -320,7 +323,10 @@ and return nil." (match-beginning 1))) (setq next-pos (- (match-end 0) 1)) (or (if (or (string-equal (match-string 1) "}") - (string-equal (match-string 1) "{")) + (string-equal (match-string 1) "{") + (string-equal (match-string 1) "-") + (string-equal (match-string 1) "+") + (string-equal (match-string 1) "*")) (save-excursion (goto-char (match-beginning 1)) (not (coq-empty-command-p))) |