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

fix(emacs/lean-info): temporary fix for NAY problem

Browse source
This commit is contained in:
Soonho Kong 2014-08-21 09:11:32 -07:00
parent 09b6fb4f7c
commit 272c463182
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -275,7 +275,7 @@
(SYNTH (lean-synth-pos info))
(IDENTIFIER (lean-identifier-pos info))
(SYMBOL (lean-symbol-pos info))
(NAY (error "no position information for NAY"))))
(NAY ())))
(defun lean-info-line-number (info)
(cl-first (lean-info-pos info)))
(defun lean-info-column (info)