From 9a09cadf8353ae9b788891363394f4937fcbf278 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 16 Dec 2011 15:09:04 +0000 Subject: 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. --- coq/coq-indent.el | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'coq/coq-indent.el') 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))) -- cgit v1.2.3