diff options
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 64 |
1 files changed, 35 insertions, 29 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e1a9a7e3..7a11a43f 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1,4 +1,4 @@ -;;; coq-syntax.el --- Font lock expressions for Coq +;;; coq-syntax.el --- Font lock expressions for Coq -*- lexical-binding:t -*- ;; This file is part of Proof General. @@ -987,14 +987,15 @@ so for the following reasons: ;; elle declare un module. ;; (la fonction vernac_declare_module dans toplevel/vernacentries) -(defun coq-count-match (regexp strg) - "Count the number of max. non-overlapping substring of STRG matching REGEXP. +(defun coq-count-match (regexp str) + "Count the number of max. non-overlapping substring of STR matching REGEXP. Empty matches are counted once." - (let ((nbmatch 0) (str strg)) - (while (and (proof-string-match regexp str) (not (string-equal str ""))) + (let ((nbmatch 0) (pos 0) (end (length str)) + (case-fold-search nil)) + (while (and (< pos end) + (string-match regexp str pos)) (cl-incf nbmatch) - (if (= (match-end 0) 0) (setq str (substring str 1)) - (setq str (substring str (match-end 0))))) + (setq pos (max (match-end 0) (1+ pos)))) nbmatch)) ;; Module and or section openings are detected syntactically. Module @@ -1009,12 +1010,16 @@ Used by `coq-goal-command-p'" (let* ((match (coq-count-match "\\_<match\\_>" str)) (with (coq-count-match "\\_<with\\_>" str)) (letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match))) - (affect (coq-count-match ":=" str))) - (and (proof-string-match "\\`\\(Module\\)\\_>" str) + (affect (coq-count-match ":=" str)) + (case-fold-search nil)) + (and (string-match "\\`\\(Module\\)\\_>" str) (= letwith affect)))) (defun coq-section-command-p (str) - (proof-string-match "\\`\\(Section\\|Chapter\\)\\_>" str)) + (let ((case-fold-search nil)) + (string-match "\\`\\(Section\\|Chapter\\)\\_>" str))) + +(defvar coq-goal-command-regexp) ;; unused anymore (for good) (defun coq-goal-command-str-p (str) @@ -1023,16 +1028,17 @@ Use ‘coq-goal-command-p’ on a span instead if possible." (let* ((match (coq-count-match "\\_<match\\_>" str)) (with (- (coq-count-match "\\_<with\\_>" str) (coq-count-match "\\_<with\\s-+signature\\_>" str))) (letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match))) - (affect (coq-count-match ":=" str))) - (and (proof-string-match coq-goal-command-regexp str) + (affect (coq-count-match ":=" str)) + (case-fold-search nil)) + (and (string-match coq-goal-command-regexp str) (not (and - (proof-string-match + (string-match (concat "\\`\\(Local\\|Definition\\|Lemma\\|Theorem\\|Fact\\|Add\\|Let\\|Program\\|Module\\|Class\\|Instance\\)\\_>") str) (not (= letwith affect)))) - (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" - str))))) + (not (string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" + str))))) ;; This is the function that tests if a SPAN is a goal start. All it ;; has to do is look at the 'goalcmd attribute of the span. @@ -1063,8 +1069,15 @@ It is used: (append coq-keywords-save-strict '("Proof")) ) +;; According to Coq, "Definition" is both a declaration and a goal. +;; It is understood here as being a goal. This is important for +;; recognizing global identifiers, see coq-global-p. +(defconst coq-save-command-regexp-strict + (proof-anchor-regexp + (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict) + "\\)"))) -(defun coq-save-command-p (span str) +(defun coq-save-command-p (_span str) "Decide whether argument is a Save command or not." (or (proof-string-match coq-save-command-regexp-strict str) (and (proof-string-match "\\`Proof\\_>" str) @@ -1151,8 +1164,10 @@ It is used: ;; FIXME: actually these are not exactly reserved keywords, find ;; another classification of keywords. (defvar coq-reserved-regexp - (concat "\\_<with\\s-+signature\\_>\\|" - (proof-ids-to-regexp coq-reserved))) + (concat "\\_<" + "\\(?:with\\s-+signature\\|" + (regexp-opt coq-reserved) "\\)" + "\\_>")) (defvar coq-state-changing-tactics (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) @@ -1276,16 +1291,6 @@ It is used: "*Font-lock table for Coq terms.") - -;; According to Coq, "Definition" is both a declaration and a goal. -;; It is understood here as being a goal. This is important for -;; recognizing global identifiers, see coq-global-p. -(defconst coq-save-command-regexp-strict - (proof-anchor-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)"))) - - (defconst coq-save-command-regexp (proof-anchor-regexp (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save) @@ -1402,7 +1407,8 @@ part of another hypothesis.") (search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t) (goto-char (match-beginning 1)) ;; if previous is a newline, don't include it i the overklay - (when (looking-back "\\s-") (goto-char (- (point) 1))) + (when (looking-back "\\s-" (1- (point))) + (goto-char (- (point) 1))) (point)))) ; if several hyp names, we name the overlays with the first hyp name (setq res |