From 9169a7aaa366d677c11ae59543e8261f4adcf429 Mon Sep 17 00:00:00 2001 From: David Christiansen Date: Wed, 14 Jun 2017 18:18:35 -0700 Subject: [PATCH] feat(emacs): Add a right-click menu to the Emacs mode The right-click menu is computed from a list of functions that produce menu items based on Lean server information. Each menu item is a string and a closure to be invoked if the menu item is selected. There are currently two menu features: "Find definition" works where M-. does, and on holes, the menu includes the hole commands from the server. --- src/emacs/lean-hole.el | 34 ++++++++++++++ src/emacs/lean-info.el | 20 +++++++++ src/emacs/lean-mode.el | 10 ++++- src/emacs/lean-right-click.el | 84 +++++++++++++++++++++++++++++++++++ src/emacs/lean-server.el | 15 +++++-- 5 files changed, 159 insertions(+), 4 deletions(-) create mode 100644 src/emacs/lean-right-click.el diff --git a/src/emacs/lean-hole.el b/src/emacs/lean-hole.el index c6400206ae..eeb8d73cf3 100644 --- a/src/emacs/lean-hole.el +++ b/src/emacs/lean-hole.el @@ -113,5 +113,39 @@ (set-marker start-marker nil) (set-marker end-marker nil)))))) +(defun lean-hole-right-click () + "Ask Lean for a list of hole commands, then ask the user which to use." + (interactive) + (let ((buf (current-buffer))) + (ignore-errors + (list + 'hole_commands + (list :file_name (buffer-file-name) + :line (line-number-at-pos) + :column (lean-line-offset)) + (cl-function + (lambda (&key start end results) + (when (and start end) + (with-current-buffer buf + (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)) + (mapcar (lambda (res) + (let ((item-name (plist-get res :name)) + (item-desc (plist-get res :description))) + (list :name + (concat item-name " — " item-desc) + :action + (lambda () + (lean-hole--command + item-name + start-marker end-marker))))) + results))))))))))) + (provide 'lean-hole) ;;; lean-hole.el ends here diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el index 1136bfe0b4..09b3ca292f 100644 --- a/src/emacs/lean-info.el +++ b/src/emacs/lean-info.el @@ -67,6 +67,26 @@ (lambda (&key record) (funcall cont record)))))) +(defun lean-info-right-click-find-definition () + "Offer to jump to definition of right-click target." + (interactive) + (list 'info + (list :file_name (buffer-file-name) + :line (line-number-at-pos) + :column (lean-line-offset)) + (cl-function + (lambda (&key record) + (let ((source-record (plist-get record :source))) + (if source-record + (let ((full-name (plist-get record :full-id))) + (list + (list :name (if full-name + (concat "Find definition of " full-name) + "Find definition") + :action (lambda () + (apply #'lean-find-definition-cont source-record))))) + (list))))))) + (cl-defun lean-find-definition-cont (&key file line column) (when (fboundp 'xref-push-marker-stack) (xref-push-marker-stack)) (when file diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index dba7be614f..2aad5fe366 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -32,6 +32,7 @@ (require 'lean-hole) (require 'lean-type) (require 'lean-message-boxes) +(require 'lean-right-click) (defun lean-compile-string (exe-name args file-name) "Concatenate exe-name, args, and file-name" @@ -86,7 +87,11 @@ (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) - (local-set-key lean-keybinding-lean-message-boxes-toggle 'lean-message-boxes-toggle)) + (local-set-key lean-keybinding-lean-message-boxes-toggle 'lean-message-boxes-toggle) + ;; This only works as a mouse binding due to the event, so it is not abstracted + ;; to avoid user confusion. + (local-set-key (kbd "") 'lean-right-click-show-menu) + ) (define-abbrev-table 'lean-abbrev-table '()) @@ -154,6 +159,9 @@ enabled and disabled respectively.") ;; server (ignore-errors (lean-server-ensure-alive)) (setq mode-name '("Lean" (:eval (lean-server-status-string)))) + ;; Right click menu sources + (setq lean-right-click-item-functions '(lean-info-right-click-find-definition + lean-hole-right-click)) ;; Flycheck (lean-flycheck-turn-on) (setq-local flycheck-disabled-checkers '()) diff --git a/src/emacs/lean-right-click.el b/src/emacs/lean-right-click.el new file mode 100644 index 0000000000..7ef76192e3 --- /dev/null +++ b/src/emacs/lean-right-click.el @@ -0,0 +1,84 @@ +;; -*- lexical-binding: t -*- +;; +;;; lean-right-click.el +;; +;; Copyright (c) 2017 David Christiansen. All rights reserved. +;; +;; Author: David Christiansen +;; Released under Apache 2.0 license as described in the file LICENSE. +;; + +;;; Code: + +(defvar lean-right-click-item-functions nil + "A list of functions to compute menu items from source locations. + +The functions take no arguments. They will be run in a context +where `current-buffer' gives the buffer in which the click +occurred. The function should return a three-element list, where +the first is a Lean server command, the second is its parameter +list, and the third is a continuation that will compute a list of +menu items. + + Each menu item is a plist that maps the key :name to the string +to show in the menu and the key :action to a zero-argument +function that implements the action.") +(make-variable-buffer-local 'lean-right-click-item-functions) + +(defvar lean-right-click--unique-val-counter 0 + "A global counter for unique values for lean-right-click.") + +(defun lean-right-click--unique-val () + "Get a unique value for internal tagging." + (cl-incf lean-right-click--unique-val-counter)) + +(defun lean-right-click--items-for-location () + "Return the menu items for point in the current buffer." + (let ((commands (cl-loop for fun in lean-right-click-item-functions + collecting (funcall fun)))) + (let ((timeout 0.15) + (items '()) + (start-time (time-to-seconds)) + (command-count (length commands)) + (commands-returned 0)) + (cl-loop for (cmd args cont) in commands + do (progn (lean-server-send-command + cmd args + (lambda (&rest result) + (setq items (append items (apply cont result))) + (cl-incf commands-returned)) + (lambda (&rest _whatever) + (cl-incf commands-returned))) + ;; This is necessary to ensure that async IO happens. + (sit-for 0.02))) + (while (and (< (time-to-seconds) (+ timeout start-time)) + (< commands-returned command-count)) + (sit-for 0.02)) + items))) + +(defun lean-right-click-show-menu (click) + "Show a menu based on the location of CLICK, computed from the `lean-right-click-functions'." + (interactive "e") + (let* ((window (posn-window (event-end click))) + (buffer (window-buffer window)) + (where (posn-point (event-end click))) + (menu-items (with-current-buffer buffer + (save-excursion + (goto-char where) + (lean-right-click--items-for-location))))) + (when menu-items + (let* ((menu (make-sparse-keymap)) + (todo (cl-loop for item in menu-items + collecting (let ((sym (lean-right-click--unique-val))) + (define-key-after menu `[,sym] + `(menu-item ,(plist-get item :name) + (lambda () (interactive))) + t) + (cons sym (plist-get item :action))))) + (selection (x-popup-menu click menu))) + (when selection + (funcall (cdr (assoc (car selection) todo)))))))) + + +(provide 'lean-right-click) +;;; lean-right-click.el ends here diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index a73731ff39..db4c14aeca 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -59,7 +59,7 @@ least the following keys: (lean-server-notify-tasks-changed sess old-tasks))) ("error" (message "error: %s" (plist-get res :message)) - ; TODO(gabriel): maybe even add the error as a message + ;; TODO(gabriel): maybe even add the error as a message (when (plist-get res :seq_num) (let ((cb (lean-server-session-pop-callback sess (plist-get res :seq_num)))) (when (cdr cb) (funcall (cdr cb) res))))) @@ -370,13 +370,21 @@ least the following keys: "Sends a command to the lean server for the current buffer, waiting for and returning the response" ;; inspired by company--force-sync (let ((res 'trash) + (ok t) (start (time-to-seconds))) - (lean-server-send-command cmd params (lambda (&rest result) (setq res result))) + (lean-server-send-command cmd params + (lambda (&rest result) (setq res result)) + (cl-function + (lambda (&key message) + (setq ok nil) + (setq res message)))) (while (eq res 'trash) (if (> (- (time-to-seconds) start) company-async-timeout) (error "Lean server timed out") (sleep-for company-async-wait))) - res)) + (if ok + res + (error res)))) (defun lean-server-sync (&optional buf) "Synchronizes the state of BUF (or the current buffer, if nil) with the lean server" @@ -396,6 +404,7 @@ least the following keys: (run-at-time "50 milliseconds" nil #'lean-server-sync (current-buffer))))) (defun lean-server-compute-roi (sess) + "Compute the region of interest for the session SESS." (--mapcat (with-current-buffer it (when (eq lean-server-session sess) (list (cons (buffer-file-name)