diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-05-02 14:06:51 +0200 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-05-02 14:06:51 +0200 |
commit | 69554c0916c0279bde6b795cb79f87b55069b25f (patch) | |
tree | edb268da72f92a38f019fbb49cd109eab464e401 | |
parent | dbfe0a4f3b7be8f18ff89f5a544cb9d9ef891b70 (diff) |
Fixing detection of symbol at point.
Quote at start of a word should not be considered part of the word.
Other characters than ' or _ are punctuation.
-rw-r--r-- | coq/coq-syntax.el | 11 | ||||
-rw-r--r-- | coq/coq.el | 15 |
2 files changed, 18 insertions, 8 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 40dac7d7..cc325c41 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1347,14 +1347,15 @@ It is used: (modify-syntax-entry ?< ".") (modify-syntax-entry ?> ".") (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?∀ "_") - (modify-syntax-entry ?∃ "_") - (modify-syntax-entry ?λ "_") ;; maybe a bad idea... lambda is a letter + (modify-syntax-entry ?_ "_") ; beware: word consituent EXCEPT in head position + (modify-syntax-entry ?\' "_") ; always word constituent + (modify-syntax-entry ?∀ ".") + (modify-syntax-entry ?∃ ".") + (modify-syntax-entry ?λ ".") ;; maybe a bad idea... lambda is a letter (modify-syntax-entry ?\| ".") ;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug + ;; Hence the coq-with-altered-syntax-table below to put "." into "_" class temporarily (modify-syntax-entry ?\. ".") (modify-syntax-entry ?\* ". 23n") @@ -816,6 +816,16 @@ Return nil if S is nil." (substring s 0 (- (length s) 1)) s)) +(defun coq-remove-heading-quote (s) + "Return the string S without its heading \"\'\" if any. +Return nil if S is nil." + (if (and s (string-match "\\`'" s)) + (substring s 1 (length s)) + s)) + +(defun coq-clean-id-at-point (s) + (coq-remove-heading-quote (coq-remove-trailing-dot s))) + (defun coq-is-symbol-or-punct (c) "Return non nil if character C is a punctuation or a symbol constituent. If C is nil, return nil." @@ -860,9 +870,8 @@ Support dot.notation.of.modules." (let* ((symb (cond ((fboundp 'symbol-near-point) (symbol-near-point)) ((fboundp 'symbol-at-point) (symbol-at-point)))) - (symbclean (when symb (coq-remove-trailing-dot (symbol-name symb))))) - (when (and symb (not (zerop (length symbclean))) - (not (coq-string-starts-with-symbol symbclean))) + (symbclean (when symb (coq-clean-id-at-point (symbol-name symb))))) + (when (and symb (not (zerop (length symbclean)))) symbclean)))) |