From eda26a90990817cd38f40bef09a93b3c46fe30cb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Dec 2015 08:11:50 -0800 Subject: [PATCH] fix(emacs/lean-company): candidate fix for #846 --- src/emacs/lean-company.el | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el index d3858d07bb..09e4fc89fd 100644 --- a/src/emacs/lean-company.el +++ b/src/emacs/lean-company.el @@ -192,7 +192,9 @@ ;; ----- (defun company-lean--need-autocomplete () (interactive) - (cond ((looking-back + (cond ((looking-back (rx "print" (+ white) "definition" (+ white) (* (not white)))) + t) + ((looking-back (rx (or "theorem" "definition" "lemma" "axiom" "parameter" "variable" "hypothesis" "conjecture" "corollary" "open")