max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(emacs): Add support for the new holes feature to Emacs

Browse source 
Add the lean-hole command to Emacs, which queries the server for a
list of relevant hole commands, presents them to the user, and
executes the one that is selected.

The default keybinding is C-c SPC.
This commit is contained in:
David Christiansen 2017-06-14 23:38:45 -07:00 • committed by Gabriel Ebner
parent 437ab1fc27
commit f3b66b3cfb
4 changed files with 123 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/emacs/README.md
View file

@ -35,6 +35,7 @@ Key Bindings and Commands
| <kbd>S-SPC</kbd> | auto complete identifiers, options, imports, etc. (`company-complete`) |
| <kbd>C-c C-k</kbd> | shows the keystroke needed to input the symbol under the cursor |
| <kbd>C-c C-x</kbd> | execute lean in stand-alone mode (`lean-std-exe`) |
| <kbd>C-c SPC</kbd> | run a command on the hole at point (`lean-hole`)
| <kbd>C-c C-g</kbd> | toggle showing current tactic proof goal (`lean-toggle-show-goal`) |
| <kbd>C-c C-n</kbd> | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) |
| <kbd>C-c C-r</kbd> | restart the lean server (`lean-server-restart`) |

117
src/emacs/lean-hole.el Normal file
View file

@ -0,0 +1,117 @@
;; -*- lexical-binding: t -*-
;;
;; Copyright (c) 2017 David Christiansen.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: David Christiansen
;;
;;; Commentary:
;; This is an interface to Lean's support for holes.
;;
;; The interface consists of two components: the hole command, which
;; collects the list of completions and the message, and a handler,
;; which selects a completion.
;;
;; For now, the only handler uses completing-read, but handlers using
;; helm or company's interface would be a good addition.
;;
;;; Code:
(require 'lean-server)
(defun lean-hole-handler-completing-read (alternatives)
"Pick a hole replacement from ALTERNATIVES with `completing-read'."
(let* ((choices (cl-loop for alt in alternatives
collect (cons (concat (plist-get alt :code)
" — "
(plist-get alt :description))
(plist-get alt :code))))
(selection (let ((this-command 'lean-hole))
(completing-read
"Response: "
choices
nil t nil nil nil t)))
(code (assoc selection choices)))
(if code
(cdr code)
(error "Didn't select a hole completion"))))
(defvar lean-hole-handler-function 'lean-hole-handler-completing-read)
(defun lean-hole--line-col->pos (line col)
"Compute the position corresponding to LINE and COL."
(save-restriction
(widen)
(save-excursion
(goto-char (point-min))
(forward-line (1- line))
(forward-char col)
(point))))
(defun lean-hole ()
"Ask Lean for a list of holes, then ask the user which to use."
(interactive)
(with-demoted-errors "lean hole: %s"
(lean-server-send-command
'hole_commands (list :file_name (buffer-file-name)
:line (line-number-at-pos)
:column (lean-line-offset))
(cl-function
(lambda (&key start end results)
(let ((start-pos (lean-hole--line-col->pos (plist-get start :line)
(plist-get start :column)))
(end-pos (lean-hole--line-col->pos (plist-get end :line)
(plist-get end :column))))
(let ((start-marker (make-marker))
(end-marker (make-marker)))
(set-marker start-marker start-pos (current-buffer))
(set-marker end-marker (1+ end-pos) (current-buffer))
(let* ((choices
(cl-loop for res in results
collect (cons (concat (plist-get res :name)
" — "
(plist-get res :description))
(plist-get res :name))))
(selection (let ((this-command 'lean-hole))
(completing-read
"Hole command: "
choices
nil t nil nil nil t)))
(code (assoc selection choices)))
(if code
(lean-hole--command (cdr code) start-marker end-marker)
(error "Didn't select a hole completion"))))))))))
;; This uses markers to ensure that if the hole moves while the
;; command is running, it is still updated.
(defun lean-hole--command (command start-marker end-marker)
"Execute COMMAND in the hole between START-MARKER and END-MARKER."
(interactive)
(with-demoted-errors "lean hole: %s"
(lean-server-send-command
'hole (list :action command
:file_name (buffer-file-name)
:line (line-number-at-pos start-marker)
:column (lean-line-offset start-marker))
(cl-function
(lambda (&key message replacements)
(let ((replacement-count (length (plist-get replacements :alternatives))))
(let ((selected-code
(cond ((= replacement-count 0)
nil)
((= replacement-count 1)
(plist-get (car (plist-get replacements :alternatives)) :code))
(t
(lean-hole-handler-completing-read
(plist-get replacements :alternatives))))))
(when selected-code
(save-excursion
(goto-char start-marker)
(delete-region start-marker (1+ end-marker))
(insert selected-code)))))
(when message
(message "%s" (s-trim message)))
(set-marker start-marker nil)
(set-marker end-marker nil))))))
(provide 'lean-hole)
;;; lean-hole.el ends here

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

@ -29,6 +29,7 @@
(require 'lean-server)
(require 'lean-flycheck)
(require 'lean-info)
(require 'lean-hole)
(require 'lean-type)
(defun lean-compile-string (exe-name args file-name)
@ -81,6 +82,7 @@
(local-set-key lean-keybinding-find-definition 'lean-find-definition)
(local-set-key lean-keybinding-tab-indent 'lean-tab-indent)
(local-set-key lean-keybinding-auto-complete 'company-complete)
(local-set-key lean-keybinding-hole 'lean-hole)
(local-set-key lean-keybinding-lean-toggle-show-goal 'lean-toggle-show-goal)
(local-set-key lean-keybinding-lean-toggle-next-error 'lean-toggle-next-error)
)

3
src/emacs/lean-settings.el
View file

@ -120,6 +120,9 @@ false (nil)."
(defcustom lean-keybinding-auto-complete (kbd "S-SPC")
"Lean Keybinding for auto completion"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-hole (kbd "C-c SPC")
"Lean Keybinding for hole manipulation"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-lean-toggle-show-goal (kbd "C-c C-g")
"Lean Keybinding for show-goal-at-pos"
:group 'lean-keybinding :type 'key-sequence)