From f3b66b3cfbb78bf18e6d7cadfa6d7cf8dd8591cd Mon Sep 17 00:00:00 2001 From: David Christiansen Date: Wed, 14 Jun 2017 23:38:45 -0700 Subject: [PATCH] feat(emacs): Add support for the new holes feature to Emacs 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. --- src/emacs/README.md | 1 + src/emacs/lean-hole.el | 117 +++++++++++++++++++++++++++++++++++++ src/emacs/lean-mode.el | 2 + src/emacs/lean-settings.el | 3 + 4 files changed, 123 insertions(+) create mode 100644 src/emacs/lean-hole.el diff --git a/src/emacs/README.md b/src/emacs/README.md index bfe6dab98f..07f601c249 100644 --- a/src/emacs/README.md +++ b/src/emacs/README.md @@ -35,6 +35,7 @@ Key Bindings and Commands | S-SPC | auto complete identifiers, options, imports, etc. (`company-complete`) | | C-c C-k | shows the keystroke needed to input the symbol under the cursor | | C-c C-x | execute lean in stand-alone mode (`lean-std-exe`) | +| C-c SPC | run a command on the hole at point (`lean-hole`) | C-c C-g | toggle showing current tactic proof goal (`lean-toggle-show-goal`) | | C-c C-n | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) | | C-c C-r | restart the lean server (`lean-server-restart`) | diff --git a/src/emacs/lean-hole.el b/src/emacs/lean-hole.el new file mode 100644 index 0000000000..fa4f826066 --- /dev/null +++ b/src/emacs/lean-hole.el @@ -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 diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 5fd9001590..f212a9d8d4 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -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) ) diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el index c8a90c2815..11ecfdad2d 100644 --- a/src/emacs/lean-settings.el +++ b/src/emacs/lean-settings.el @@ -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)