From 6c2e576dff076da8132d546f041dba8b5e79833b Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Mon, 29 Sep 2014 12:49:00 -0700 Subject: [PATCH] fix(emacs/lean-mode): trigger eri-indent only at the beginning of line --- src/emacs/lean-mode.el | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 1808236012..be56ef27f3 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -66,16 +66,21 @@ (backward-char 1) (if (looking-at "->") t nil)))))) +(defun lean-tab-indent () + (cond ((looking-back (rx line-start (* white))) + (eri-indent)) + (t (indent-for-tab-command)))) + (defun lean-tab-indent-or-complete () (interactive) (if (minibufferp) (minibuffer-complete) (cond ((and lean-company-use (company-lean--check-prefix)) (company-complete-common)) - (lean-company-use (eri-indent)) + (lean-company-use (lean-tab-indent)) ((lean-check-expansion) (completion-at-point-functions)) - (t (eri-indent))))) + (t (lean-tab-indent))))) (defun lean-set-keys () (local-set-key "\C-c\C-x" 'lean-std-exe)