aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2016-05-16 19:00:26 -0400
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2016-05-16 19:00:26 -0400
commit3bcc3c41799dd8b8bf50d182346d962b67f396ab (patch)
tree1d3c694348cbe46986ed41bbd3189e746e35d3d7 /coq/coq.el
parent4346278e5ae54fe46a3dd04cb92892a0c9e045c0 (diff)
parent9ae103b86dd3cdfc3e6e6326ebc1a8f803e50f7d (diff)
Merge branch 'master' of github.com:ProofGeneral/PG
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el15
1 files changed, 12 insertions, 3 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 4921bdaf..f7b419fc 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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))))