michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(emacs/lean-company): candidate fix for #846

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-11 08:11:50 -08:00
parent 2b1e7e7759
commit eda26a9099
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/emacs/lean-company.el
View file

@ -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")