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

feat(emacs/lean-company): "c-u TAB" asks filter for FINDG

Browse source
This commit is contained in:
Soonho Kong 2014-09-09 13:00:34 -07:00
parent ee196bbf1a
commit c26f39b86e
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

@ -49,7 +49,9 @@ triggers a completion immediately."
(lean-server-send-cmd-sync (lean-cmd-wait)) (lean-server-send-cmd-sync (lean-cmd-wait))
(cond (cond
((looking-at (rx symbol-start "_")) ((looking-at (rx symbol-start "_"))
(setq pattern (read-string "Filter for find declarations (e.g: +intro -and): " "" nil "")) (setq pattern (if current-prefix-arg
(read-string "Filter for find declarations (e.g: +intro -and): " "" nil "")
""))
(lean-server-send-cmd-sync (lean-cmd-findg line-number column-number pattern) (lean-server-send-cmd-sync (lean-cmd-findg line-number column-number pattern)
(lambda (candidates) (lambda (candidates)
(lean-server-debug "executing continuation for FINDG") (lean-server-debug "executing continuation for FINDG")