Use prop-menu.el to show popups

This has a few advantages over the old way of sticking a keymap property on regions of text: 1. The semantic properties of the text are decoupled from the generation of the menus, allowing them to be different in the editing mode than they are in the info modes. This will eventually enable things like right-clicking a pattern variable to case split. 2. Menus can take multiple kinds of information into account, merging e.g. the menu for an error annotation with the menu for a name annotation. 3. A keyboard-accessible contextual menu is provided, bound to C-c C-SPC.
idris-hackers · Jun 28, 2015 · 8d4e082 · 8d4e082
1 parent e2aaa7a
commit 8d4e082
Show file tree

Hide file tree

Showing 13 changed files with 138 additions and 162 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -50,10 +50,13 @@ script:
       - popd
 
       # emacs 24.3
+      - make getdeps
       - make build
       - make test
       - make clean
 
       # emacs 24.4
+      - make getdeps EMACS=/usr/local/emacs-24.4/bin/emacs
       - make build EMACS=/usr/local/emacs-24.4/bin/emacs
       - make test EMACS=/usr/local/emacs-24.4/bin/emacs
+      - make clean
diff --git a/Makefile b/Makefile
@@ -1,9 +1,9 @@
 # Makefile for idris-mode, to run tests and ensure dependencies are in order
 # Portions based on the Makefile for Proof General
 
-EMACS=emacs
+EMACS=emacs24
 
-BATCHEMACS=$(EMACS) --batch --no-site-file -q -eval '(add-to-list (quote load-path) "${PWD}/")'
+BATCHEMACS=$(EMACS) --batch --no-site-file -q -eval '(add-to-list (quote load-path) "${PWD}/")' -eval '(add-to-list (quote package-archives) (quote ("melpa" . "http://melpa.org/packages/")) t)' -eval '(package-initialize)'
 
 BYTECOMP = $(BATCHEMACS) -eval '(progn (require (quote bytecomp)) (setq byte-compile-warnings t) (setq byte-compile-error-on-warn t))' -f batch-byte-compile
 
@@ -41,4 +41,7 @@ clean:
 	-rm -f $(OBJS)
 	-rm -f test-data/*ibc
 
+getdeps:
+	$(BATCHEMACS) -eval '(package-install (quote prop-menu))'
+
 .PHONY: clean build test
diff --git a/idris-commands.el b/idris-commands.el
@@ -23,6 +23,8 @@
 ;; the Free Software Foundation, Inc., 59 Temple Place - Suite 330,
 ;; Boston, MA 02111-1307, USA.
 
+;;; Code:
+
 (require 'idris-core)
 (require 'idris-settings)
 (require 'inferior-idris)
@@ -53,7 +55,6 @@
     (delete-overlay idris-loaded-region-overlay))
   (setq idris-loaded-region-overlay nil))
 
-
 (defun idris-make-clean ()
   (setq idris-buffer-dirty-p nil))
 
@@ -827,122 +828,6 @@ means to not ask for confirmation."
           (delete-file ibc)
           (message "%s deleted" ibc))))))
 
-(defun idris-make-namespace-menu (namespace &optional file)
-  "Create a right-click menu for NAMESPACE (optionally with source FILE)."
-  (let ((menu (make-sparse-keymap)))
-    (define-key menu [idris-namespace-menu-browse-namespace]
-      `(menu-item ,(concat "Browse " namespace)
-                  (lambda () (interactive))))
-    (when (and (stringp file) (file-exists-p file))
-      (define-key menu [idris-namespace-menu-visit-file]
-        `(menu-item ,(concat "Edit " file)
-                    (lambda () (interactive)))))
-    menu))
-
-
-(defun idris-make-namespace-keymap (namespace &optional file)
-  "Create a keymap that shows a right-click menu for NAMESPACE (optionally pointing at FILE)."
-  (let ((map (make-sparse-keymap)))
-    (define-key map [mouse-3]
-      (lambda ()
-        (interactive)
-        (let* ((menu (idris-make-namespace-menu namespace file))
-               (selection (x-popup-menu t menu)))
-          (cond ((and (equal selection '(idris-namespace-menu-browse-namespace))
-                      namespace)
-                 (idris-browse-namespace namespace))
-                ((and (equal selection '(idris-namespace-menu-visit-file))
-                      (stringp file))
-                 (find-file file))
-                (t (message "%S" selection))))))
-    map))
-
-(defun idris-make-ref-menu (_name &optional namespace)
-  (let ((menu (make-sparse-keymap)))
-    (define-key menu [idris-ref-menu-get-type]
-      `(menu-item "Get type"
-                  (lambda () (interactive)))) ; x-popup-menu doesn't run cmds
-    (define-key-after menu [idris-ref-menu-get-docs]
-      `(menu-item "Get documentation"
-                  (lambda () (interactive)))) ; x-popup-menu doesn't run cmds
-    (define-key-after menu [idris-ref-menu-print-definition]
-      `(menu-item "Get definition"
-                  (lambda () (interactive))))
-    (define-key-after menu [idris-ref-menu-who-calls]
-      `(menu-item "Who calls?"
-                  (lambda () (interactive))))
-    (define-key-after menu [idris-ref-menu-calls-who]
-      `(menu-item "Calls who?"
-                  (lambda () (interactive))))
-    (when (stringp namespace)
-      (define-key-after menu [idris-ref-menu-browse-namespace]
-        `(menu-item ,(concat "Browse " namespace)
-                    (lambda () (interactive)))))
-    menu))
-
-(defun idris-make-ref-menu-keymap (name &optional namespace)
-  "Create a keymap that shows a right-click menu for a reference to NAME (optionally in namespace NAMESPACE)."
-  (let ((map (make-sparse-keymap)))
-    (define-key map [mouse-3]
-      (lambda () (interactive)
-        (let ((selection (x-popup-menu t (idris-make-ref-menu name namespace))))
-          (cond ((equal selection '(idris-ref-menu-get-type))
-                 (idris-info-for-name :type-of name))
-                ((equal selection '(idris-ref-menu-get-docs))
-                 (idris-info-for-name :docs-for name))
-                ((equal selection '(idris-ref-menu-print-definition))
-                 (idris-info-for-name :print-definition name))
-                ((equal selection '(idris-ref-menu-who-calls))
-                 (idris-who-calls-name name))
-                ((equal selection '(idris-ref-menu-calls-who))
-                 (idris-name-calls-who name))
-                ((and (equal selection '(idris-ref-menu-browse-namespace))
-                      namespace)
-                 (idris-browse-namespace namespace))
-                (t (message "%S" selection))))))
-    map))
-
-(defun idris-make-hole-menu (_name)
-  (let ((menu (make-sparse-keymap)))
-    (define-key menu [idris-hole-menu-prover]
-      `(menu-item "Launch prover"
-                  (lambda () (interactive))))
-    (when idris-enable-elab-prover
-      (define-key menu [idris-hole-menu-elab]
-        `(menu-item "Launch interactive elaborator"
-                    (lambda () (interactive)))))
-    menu))
-
-(defun idris-make-hole-keymap (name)
-  (let ((map (make-sparse-keymap)))
-    (define-key map [mouse-3]
-      (lambda () (interactive)
-        (let ((selection (x-popup-menu t (idris-make-hole-menu name))))
-          (cond ((equal selection '(idris-hole-menu-prover))
-                 (idris-prove-hole name))
-                ((equal selection '(idris-hole-menu-elab))
-                 (idris-prove-hole name t))
-                (t (message "%S" selection))))))
-    map))
-
-(defun idris-make-error-menu (_err)
-  (let ((menu (make-sparse-keymap)))
-    (define-key menu [idris-err-menu-view]
-      `(menu-item "View error"
-                  (lambda () (interactive)))) ; x-popup-menu doesn't run cmds
-    menu))
-
-(defun idris-make-error-keymap (err)
-  (let ((map (make-sparse-keymap)))
-    (define-key map [mouse-3]
-      (lambda () (interactive)
-        (let ((selection (x-popup-menu t (idris-make-error-menu err))))
-          (cond ((equal selection '(idris-err-menu-view))
-                 (idris-info-for-name :error-pprint err))
-                (t (message "%S" selection))))))
-    (define-key map (kbd "RET")
-      (lambda () (interactive) (idris-info-for-name :error-pprint err)))
-    map))
 
 (defun idris-make-term-menu (_term)
   "Make a menu for the widget for some term."
@@ -1230,5 +1115,58 @@ of the term to replace."
                (not idris-prover-currently-proving))
       (idris-eval `(:interpret ,command) t))))
 
+;;; Computing a menu with these commands
+(defun idris-context-menu-items (plist)
+  "Compute a contextual menu based on the Idris semantic decorations in PLIST."
+  (let ((ref (plist-get plist 'idris-ref))
+        (ref-style (plist-get plist 'idris-ref-style))
+        (namespace (plist-get plist 'idris-namespace))
+        (source-file (plist-get plist 'idris-source-file)))
+    (append
+     (when ref
+       (append (list (list "Get type"
+                           (lambda ()
+                             (interactive)
+                             (idris-info-for-name :type-of ref))))
+               (cond ((member ref-style
+                              '(:type :data :function))
+                      (list
+                       (list "Get docs"
+                             (lambda ()
+                               (interactive)
+                               (idris-info-for-name :docs-for ref)))
+                       (list "Get definition"
+                             (lambda ()
+                               (interactive)
+                               (idris-info-for-name :print-definition ref)))
+                       (list "Who calls?"
+                             (lambda ()
+                               (interactive)
+                               (idris-who-calls-name ref)))
+                       (list "Calls who?"
+                             (lambda ()
+                               (interactive)
+                               (idris-name-calls-who ref)))))
+                     ((equal ref-style :metavar)
+                      (cons (list "Launch prover"
+                                  (lambda ()
+                                    (interactive)
+                                    (idris-prove-hole ref)))
+                            (when idris-enable-elab-prover
+                              (list (list "Launch interactive elaborator"
+                                          (lambda ()
+                                            (interactive)
+                                            (idris-prove-hole ref t))))))))))
+     (when namespace
+       (list (list (concat "Browse " namespace)
+                   (lambda ()
+                     (interactive)
+                     (idris-browse-namespace namespace)))))
+     (when (and namespace source-file)
+       (list (list (concat "Edit " source-file)
+                   (lambda ()
+                     (interactive)
+                     (find-file source-file))))))))
 
 (provide 'idris-commands)
+;;; idris-commands.el ends here
diff --git a/idris-common-utils.el b/idris-common-utils.el
@@ -1,8 +1,8 @@
 ;;; idris-common-utils.el --- Useful utilities -*- lexical-binding: t -*-
 
-;; Copyright (C) 2013 Hannes Mehnert
+;; Copyright (C) 2013-2015 Hannes Mehnert and David Raymond Christiansen
 
-;; Author: Hannes Mehnert <hannes@mehnert.org>
+;; Author: Hannes Mehnert <hannes@mehnert.org> and David Raymond Christiansen <david@davidchristiansen.dk>
 
 ;; License:
 ;; Inspiration is taken from SLIME/DIME (http://common-lisp.net/project/slime/) (https://github.com/dylan-lang/dylan-mode)
@@ -56,7 +56,8 @@ strings that are suitable arguments to `start-process'.")
 This is used to load resource files such as images.  The default
 value is automatically computed from the location of the Emacs
 Lisp package.")
-(setq idris-mode-path (file-name-directory load-file-name))
+(when load-file-name ;; guard to allow M-x eval-buffer
+  (setq idris-mode-path (file-name-directory load-file-name)))
 
 (defun idris-buffer-name (type)
   (cl-assert (keywordp type))
@@ -115,11 +116,7 @@ inserted text (that is, relative to point prior to insertion)."
                                           (+ ,start begin length)
                                           props))))))
 
-;;; Take care of circular dependency issue
-(autoload 'idris-make-ref-menu-keymap "idris-commands.el")
-(autoload 'idris-make-hole-keymap "idris-commands.el")
-(autoload 'idris-make-error-keymap "idris-commands.el")
-(autoload 'idris-make-namespace-keymap "idris-commands.el")
+;;; TODO: Take care of circular dependency issue
 (autoload 'idris-eval "inferior-idris.el")
 
 (defun idris-make-link-keymap (url)
@@ -227,30 +224,22 @@ inserted text (that is, relative to point prior to insertion)."
          (image (assoc :image props)))
     (append '(rear-nonsticky t)
             (cond (name
-                   (cond ((and (member (cadr decor)
-                                       '(:type :data :function))
-                               name)
-                          (list 'idris-ref (cadr name)
-                                'keymap (idris-make-ref-menu-keymap
-                                         (cadr name)
-                                         (if namespace
-                                             (cadr namespace)
-                                           nil))))
-                         ((equal (cadr decor) :metavar)
-                          (list 'idris-ref (cadr name)
-                                'keymap (idris-make-hole-keymap (cadr name))))
-                         (t nil)))
+                   (if (and (member (cadr decor)
+                                    '(:type :data :function :metavar))
+                            name)
+                       (list 'idris-ref (cadr name)
+                             'idris-ref-style (cadr decor))
+                     ()))
                   (namespace
-                   (cond ((or (equal (cadr decor) :module)
-                              (equal (cadr decor) :namespace))
-                          (list 'keymap (idris-make-namespace-keymap
-                                         (cadr namespace)
-                                         (if source-file
-                                             (cadr source-file)
-                                           nil))))
-                         (t nil)))
+                   (if (or (equal (cadr decor) :module)
+                           (equal (cadr decor) :namespace))
+                       (append (list 'idris-namespace (cadr namespace))
+                               (when source-file
+                                 (list 'idris-source-file (cadr source-file))))
+                     ()))
                   (link-href
-                   (list 'keymap (idris-make-link-keymap (cadr link-href))))
+                   (list 'keymap (idris-make-link-keymap (cadr link-href))
+                         'idris-url (cadr link-href)))
                   (image
                    (list 'display
                          `(image :type imagemagick
@@ -261,8 +250,7 @@ inserted text (that is, relative to point prior to insertion)."
                 (list 'idris-tt-term (cadr term))
               ())
             (if idris-err
-                (list 'idris-tt-error (cadr idris-err)
-                      'keymap (idris-make-error-keymap (cadr idris-err)))
+                (list 'idris-tt-error (cadr idris-err))
               ())
             (idris-semantic-properties-help-echo props)
             (idris-semantic-properties-face props))))

diff --git a/idris-compat.el b/idris-compat.el
@@ -1,7 +1,9 @@
 ;;; idris-compat.el --- compatibility functions for Emacs 24.1 -*- lexical-binding: t -*-
 
+;;; Commentary:
 ;; This file defines defvar-local, which was introduced in Emacs 24.3, and string-suffix-p, from Emacs 24.4.
 
+;;; Code:
 (unless (fboundp 'defvar-local)
   (defmacro defvar-local (var val &optional docstring)
     `(progn
@@ -20,3 +22,4 @@ attention to case differences."
                                   string start-pos nil ignore-case))))))
 
 (provide 'idris-compat)
+;;; idris-compat.el ends here
diff --git a/idris-core.el b/idris-core.el
@@ -23,11 +23,14 @@
 ;; the Free Software Foundation, Inc., 59 Temple Place - Suite 330,
 ;; Boston, MA 02111-1307, USA.
 
+;;; Code:
 (require 'idris-compat)
-(provide 'idris-core)
 
 (defun idris-is-ident-char-p (ch)
   (or (and (<= ?a ch) (<= ch ?z))
       (and (<= ?A ch) (<= ch ?Z))
       (and (<= ?0 ch) (<= ch ?9))
       (= ch ?_)))
+
+(provide 'idris-core)
+;;; idris-core.el ends here
diff --git a/idris-hole-list.el b/idris-hole-list.el
@@ -24,6 +24,7 @@
 ;; Boston, MA 02111-1307, USA.
 
 (require 'cl-lib)
+(require 'prop-menu)
 
 (require 'idris-core)
 (require 'idris-keys)
@@ -62,7 +63,8 @@
 (define-derived-mode idris-hole-list-mode fundamental-mode "Idris Holes"
   "Major mode used for transient Idris hole list buffers
    \\{idris-hole-list-mode-map}
-Invoces `idris-hole-list-mode-hook'.")
+Invoces `idris-hole-list-mode-hook'."
+  (setq-local prop-menu-item-functions '(idris-context-menu-items)))
 
 (defun idris-hole-list-buffer ()
   "Return the Idris hole buffer, creating one if there is not one"

diff --git a/idris-info.el b/idris-info.el
@@ -25,6 +25,7 @@
 ;; that buffer to a minimum.
 
 ;;; Code:
+(require 'prop-menu)
 (require 'idris-core)
 (require 'idris-common-utils)
 
@@ -89,7 +90,8 @@ Following the behavior of Emacs help buffers, the future is deleted."
 (define-derived-mode idris-info-mode fundamental-mode "Idris Info"
   "Major mode used for transient Idris information buffers
     \\{idris-info-mode-map}
-Invokes `idris-info-mode-hook'.")
+Invokes `idris-info-mode-hook'."
+  (set (make-local-variable 'prop-menu-item-functions) '(idris-context-menu-items)))
 ; if we use view-mode here, our key binding q would be shadowed.
 
 (defun idris-info-buffer ()

diff --git a/idris-keys.el b/idris-keys.el
@@ -69,7 +69,9 @@
 
 (defun idris-define-general-keys (map)
   "Define keys that are generally useful for all Idris modes in the keymap MAP."
-  (define-key map (kbd "C-c C-z") 'idris-pop-to-repl))
+  (define-key map (kbd "C-c C-z") 'idris-pop-to-repl)
+  (define-key map (kbd "<mouse-3>") 'prop-menu-show-menu)
+  (define-key map (kbd "C-c C-SPC") 'prop-menu-by-completing-read))
 
 (defun idris-define-active-term-keys (map)
   "Define keys for manipulating active terms in the keymap MAP."