diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2012-09-07 10:14:50 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2012-09-07 10:14:50 +0000 |
commit | 45bc0e01e199acfa8dce1ba253d81f7248cd112b (patch) | |
tree | 2d8e06ae78f2c9c4e2ed8c91e2676001f3ee4bee | |
parent | 499893e8b94962c8a963d95b7144a1d0f8f33f11 (diff) |
Fixed a bug with coq symbol detection at point. Now dot notation.are supported.
-rw-r--r-- | coq/coq.el | 23 |
1 files changed, 19 insertions, 4 deletions
@@ -653,15 +653,30 @@ If locked span already has a state number, then do nothing. Also updates ) ) +;; remove trailing dot if any. +(defun coq-id-at-point () + (let* ((symb + (symbol-name (cond + ((fboundp 'symbol-near-point) (symbol-near-point)) + ((fboundp 'symbol-at-point) (symbol-at-point)) + (t 'nothing)))) + (symbclean (if symb + (if (string-match "\\.\\>" symb) + (substring symb 0 (- (length symb) 1)) + symb) + nil))) + (if (zerop (length symbclean)) nil symbclean))) + + (defun coq-guess-or-ask-for-string (s &optional dontguess) - (let ((guess + "Get coq id at point." + (let* ((dummy (modify-syntax-entry ?\. "w")) + (guess (cond (dontguess nil) ((use-region-p) (buffer-substring-no-properties (region-beginning) (region-end))) - ((fboundp 'symbol-near-point) (symbol-near-point)) - ((fboundp 'symbol-at-point) (symbol-at-point))))) - (if (and guess (symbolp guess)) (setq guess (symbol-name guess))) + (t (coq-id-at-point))))) (read-string (if guess (concat s " (default " guess "): ") (concat s ": ")) nil 'proof-minibuffer-history guess))) |