max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(emacs/lean-info): push marker to go back after find-definition

Browse source
This commit is contained in:
Gabriel Ebner 2016-11-08 12:34:18 -05:00 • committed by Leonardo de Moura
parent 25803e745c
commit cd32335c51
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/emacs/lean-info.el
View file

@ -56,6 +56,7 @@
(funcall cont record))))))
(cl-defun lean-find-definition-cont (&key file line column)
(when (fboundp 'xref-push-marker-stack) (xref-push-marker-stack))
(when file
(find-file file))
(goto-char (point-min))