From 70dcc2e122cd7fef79dc863245bddc5c4e24ad0d Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Tue, 9 Sep 2014 13:22:07 -0700 Subject: [PATCH] fix(emacs): use looking-at instead of char-after --- src/emacs/lean-info.el | 5 ++--- src/emacs/lean-server.el | 6 ++---- src/emacs/lean-type.el | 2 +- 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el index 2ff647407..6d2fcb3f3 100644 --- a/src/emacs/lean-info.el +++ b/src/emacs/lean-info.el @@ -640,11 +640,10 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim." (let* ((file-name (buffer-file-name)) (line-number (line-number-at-pos)) (column-number (current-column)) - (cur-char (char-after (point))) - (cmd (cond ((and cur-char (char-equal cur-char ?\()) + (cmd (cond ((looking-at "(") (lean-cmd-info line-number column-number)) ;; TODO(soonhok): give information on '(' - ;; ((char-equal cur-char ?\)) + ;; ((looking-at ")") ;; (let ((begin-pos (lean-get-begin-paren-pos))) ;; (lean-cmd-info (car begin-pos) (cdr begin-pos)))) (t (lean-cmd-info line-number))))) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index 4b2daffb1..10a658d2d 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -446,10 +446,8 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. (defun lean-server-get-info-record-at-pos (body) (let* ((file-name (buffer-file-name)) - (column (current-column)) - (cur-char (char-after (point)))) - (when (and cur-char - (--any? (char-equal cur-char it) '(?\s ?\t ?\, ?\) ?\} ?\])) + (column (current-column))) + (when (and (looking-at (or white "," ")" "}" "]")) (> column 1)) (setq column (1- column))) (lean-info-record-parse body file-name column))) diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index f93f09d89..67a789644 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -23,7 +23,7 @@ (replace-regexp-in-string "?M_[0-9]+" "_" (lean-info-synth-body-str synth)))) (when (search " " synth-str) (setq synth-str (concat "(" synth-str ")"))) - (when (char-equal (char-after (point)) ?_) + (when (looking-at "_") (delete-forward-char 1) (insert synth-str))))))