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)