From 7c9b364957c323a4b60a79005fdecae4017206a4 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 27 Mar 2015 11:37:47 -0400 Subject: [PATCH] fix(emacs/lean-info): lean-info-list-parse close #302 --- src/emacs/lean-info.el | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el index c5fdaf203..d4676b158 100644 --- a/src/emacs/lean-info.el +++ b/src/emacs/lean-info.el @@ -396,7 +396,10 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim." start-column) (cond ;; 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 (lean-info-list-filter info-list (save-excursion