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

feat(emacs/lean-mode): add lean-show-goal-at-pos

Browse source 
which is bound to 'C-c C-g' by default. Depending on the current char,
it invokes lean-server with either '--goal' or '--hole' option.

close #749
This commit is contained in:
Soonho Kong 2015-07-28 14:16:13 -07:00
parent 8ee1d35bed
commit 0fed6129df
2 changed files with 23 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/emacs/lean-mode.el
View file

@ -145,6 +145,23 @@ will be flushed everytime it's executed."
(set-process-coding-system p 'utf-8 'utf-8)
(set-process-query-on-exit-flag p nil)))
(defun lean-show-goal-at-pos ()
"Show goal at the current point. If the current point is a
placeholder, call lean-server with --hole option, otherwise call
lean-server with --goal option"
(interactive)
(cond ((and (eq (char-after) ?_) ;; 1. at _
(not (lean-in-comment-p)) ;; 2. not in comment
(or (bolp) ;; 3. either beginning of line
(let ((cb (char-before))) ;; or whitespace
(or (char-equal cb ?\s)
(char-equal cb ?\t)
(char-equal cb ?\n)
(char-equal cb ?\r))))
(lean-exec-at-pos "lean-hole" "*Lean Goal*" "--hole"))
(t
(lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))))
(defun lean-std-exe ()
(interactive)
(lean-execute))
@ -186,11 +203,7 @@ will be flushed everytime it's executed."
(local-set-key "\C-c\C-r" 'lean-server-restart-process)
(local-set-key "\M-." 'lean-find-tag)
(local-set-key (kbd "TAB") 'lean-tab-indent-or-complete)
(lean-define-key-binding "\C-c\C-p"
'(lean-exec-at-pos "lean-hole" "*Lean Goal*" "--hole"))
(lean-define-key-binding "\C-c\C-g"
'(lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))
)
(lean-define-key-binding "\C-c\C-g" '(lean-show-goal-at-pos)))
(defun lean-define-key-binding (key cmd)
(local-set-key key `(lambda () (interactive) ,cmd)))

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

@ -194,4 +194,9 @@
'hott)
(t 'standard))))
(defun lean-in-comment-p ()
"t if a current point is inside of comment block
nil otherwise"
(nth 4 (syntax-ppss)))
(provide 'lean-util)