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

fix(emacs/lean-info): lean-info-list-parse

Browse source 
close #302
This commit is contained in:
Soonho Kong 2015-03-27 11:37:47 -04:00
parent 5c1d7458b5
commit 7c9b364957
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -396,7 +396,10 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
start-column) start-column)
(cond (cond
;; Proof State Case ;; Proof State Case
((and column-number (or (looking-at ",") (looking-back (rx "," (* white))))) ((and column-number (or (looking-at ",")
(and
(looking-at (rx white))
(looking-back (rx "," (* white))))))
;; Find a position of "," and filter the info-list to extract proofstate info ;; Find a position of "," and filter the info-list to extract proofstate info
(lean-info-list-filter info-list (lean-info-list-filter info-list
(save-excursion (save-excursion