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

feat(emacs): extract proof state information attached to ","

Browse source
This commit is contained in:
Soonho Kong 2014-10-28 14:04:53 -07:00
parent fdf5f3ff8a
commit 53f79ec9c2
2 changed files with 12 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -370,6 +370,8 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
(let ((info-list (lean-info-list-parse-string str))
start-column)
(cond
((and column-number (or (looking-at ",") (looking-back (rx "," (* white)))))
info-list)
;; When file-name/column-number is specified, try to start-column of id/symbol
((and file-name column-number)
(setq start-column (lean-info-list-find-start-column info-list file-name column-number))
@ -497,12 +499,10 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
(let* ((file-name (buffer-file-name))
(line-number (line-number-at-pos))
(column-number (lean-line-offset))
(cmd (cond ((looking-at "(")
(cmd (cond ((or (looking-at "(") (looking-at ","))
(lean-cmd-info line-number column-number))
;; TODO(soonhok): give information on '('
;; ((looking-at ")")
;; (let ((begin-pos (lean-get-begin-paren-pos)))
;; (lean-cmd-info (car begin-pos) (cdr begin-pos))))
((and (eolp) (looking-back ",") (> column-number 1))
(lean-cmd-info line-number (1- column-number)))
(t (lean-cmd-info line-number)))))
(lean-debug "get-info-record-at-point: %S" cmd)
(lean-server-check-current-file file-name)

12
src/emacs/lean-server.el
View file

@ -481,11 +481,13 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
(defun lean-server-get-info-record-at-pos (body)
(let* ((file-name (buffer-file-name))
(column (lean-line-offset)))
(when (and (or (looking-at (rx (or white "," ")" "}" "]")))
(eolp))
(> column 1))
(setq column (1- column)))
(lean-info-record-parse body file-name column)))
(save-excursion
(when (and (or (looking-at (rx (or white ")" "}" "]")))
(eolp))
(> column 1))
(setq column (1- column))
(backward-char 1))
(lean-info-record-parse body file-name column))))
(defun lean-server-event-handler ()
"Process an item from async-task-queue.