diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-05-16 19:00:26 -0400 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-05-16 19:00:26 -0400 |
commit | 3bcc3c41799dd8b8bf50d182346d962b67f396ab (patch) | |
tree | 1d3c694348cbe46986ed41bbd3189e746e35d3d7 /coq/coq.el | |
parent | 4346278e5ae54fe46a3dd04cb92892a0c9e045c0 (diff) | |
parent | 9ae103b86dd3cdfc3e6e6326ebc1a8f803e50f7d (diff) |
Merge branch 'master' of github.com:ProofGeneral/PG
Diffstat (limited to 'coq/coq.el')
-rw-r--r-- | coq/coq.el | 15 |
1 files changed, 12 insertions, 3 deletions
@@ -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)))) |