From 1854459fef368dfc8ca870792e7e3b065a2241c6 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Sat, 15 Dec 2018 20:03:43 -0500 Subject: Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev. Fix a few more cl.el leftovers. Get rid of remaining use of iso-2022. Use SMIE unconditionally. * coq/coq-abbrev.el: Use lexical-binding. (coq-install-abbrevs): Delete, only keep the relevant contents. (proof-defstringset-fn): Remove. Fold changes into the main version. * coq/coq-indent.el (coq-find-real-start): Use forward-comment. * coq/coq-smie.el: Use lexical-binding. Assume `smie` is available. (coq--string-suffix-p): Rename from coq-string-suffix-p. Use string-suffix-p for it when available. (string-suffix-p): Never define here. Change all users to use coq--string-suffix-p instead. (coq-smie-.-deambiguate): Use forward-comment. Remove unused var `beg`. (coq-backward-token-fast-nogluing-dot-friends) (coq-forward-token-fast-nogluing-dot-friends): Remove unused var `tok-other`. (coq-smie-search-token-backward): Remove unused var `p`. (coq-smie-:=-deambiguate, coq-smie-backward-token): Prefer char-before over looking-back. (coq-smie-rules): Use `pcase` over deprecated cl's `case`. * coq/coq-syntax.el: Use lexical-binding. (coq-count-match): Rewrite so it doesn't do needless heap-allocation. (coq-module-opening-p, coq-section-command-p, coq-goal-command-str-p): Use case-fold-search rather than proof-string-match. (coq-goal-command-regexp): Forward-declare. (coq-save-command-regexp-strict): Move before first use. (coq-reserved-regexp): Use a single \_< ... \_>. (coq-detect-hyps-positions): Limit search for looking-back. * coq/coq.el: Remove SMIE declarations since SMIE is always used. (coq-use-smie): Remove, unused. (coq-smie): Always require. * generic/pg-pbrpm.el: Fix leftover cl.el uses. * generic/proof-utils.el (proof-defstringset-fn): Fix copy&paste error in the docstring, improve interactive prompt. * lib/maths-menu.el: Use utf-8 and lexical-binding. --- coq/coq-syntax.el | 64 ++++++++++++++++++++++++++++++------------------------- 1 file changed, 35 insertions(+), 29 deletions(-) (limited to 'coq/coq-syntax.el') 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 "\\_" str)) (with (coq-count-match "\\_" str)) (letwith (+ (coq-count-match "\\_" 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 "\\_" str)) (with (- (coq-count-match "\\_" str) (coq-count-match "\\_" str))) (letwith (+ (coq-count-match "\\_" 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 "\\_\\|" - (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 -- cgit v1.2.3