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

fix(emacs/lean-info): extract proofstate info by using pos of ","

Browse source 
fix #302
This commit is contained in:
Soonho Kong 2015-03-25 12:36:15 -04:00
parent ca81e9bee2
commit 4c434f4c02
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -395,8 +395,14 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
(let ((info-list (lean-info-list-parse-string str)) (let ((info-list (lean-info-list-parse-string str))
start-column) start-column)
(cond (cond
;; Proof State Case
((and column-number (or (looking-at ",") (looking-back (rx "," (* white))))) ((and column-number (or (looking-at ",") (looking-back (rx "," (* white)))))
info-list) ;; Find a position of "," and filter the info-list to extract proofstate info
(lean-info-list-filter info-list
(save-excursion
(unless (looking-at ",")
(search-backward ","))
(current-column))))
;; When file-name/column-number is specified, try to start-column of id/symbol ;; When file-name/column-number is specified, try to start-column of id/symbol
((and file-name column-number) ((and file-name column-number)
(setq start-column (lean-info-list-find-start-column info-list file-name column-number)) (setq start-column (lean-info-list-find-start-column info-list file-name column-number))