This repository has been archived by the owner on Aug 5, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 17
/
helm-lean.el
69 lines (55 loc) · 2.51 KB
/
helm-lean.el
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
;;; helm-lean.el --- Helm interfaces for lean-mode -*- lexical-binding: t -*-
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Author: Leonardo de Moura <[email protected]>
;; Soonho Kong <[email protected]>
;; Gabriel Ebner <[email protected]>
;; Sebastian Ullrich <[email protected]>
;; Maintainer: Sebastian Ullrich <[email protected]>
;; Created: Jan 09, 2014
;; Keywords: languages
;; Package-Requires: ((emacs "24.3") (dash "2.18.0") (helm "2.8.0") (lean-mode "3.3.0"))
;; URL: https://github.com/leanprover/lean-mode
;; Released under Apache 2.0 license as described in the file LICENSE.
;;; Commentary:
;; Currently provides an interface for looking up Lean definitions by name
;;; Code:
(require 'dash)
(require 'helm)
(require 'lean-server)
(defcustom helm-lean-keybinding-helm-lean-definitions (kbd "C-c C-d")
"Lean Keybinding for helm-lean-definitions"
:group 'lean-keybinding :type 'key-sequence)
(defun helm-lean-definitions-format-candidate (c)
`(,(format "%s : %s %s"
(propertize (plist-get c :text) 'face font-lock-variable-name-face)
(plist-get c :type)
(propertize (plist-get (plist-get c :source) :file) 'face font-lock-comment-face))
. ,c))
(defun helm-lean-definitions-candidates ()
(with-helm-current-buffer
(let* ((response (lean-server-send-synchronous-command 'search (list :query helm-pattern)))
(results (plist-get response :results))
(results (-filter (lambda (c) (plist-get c :source)) results))
(candidates (-map 'helm-lean-definitions-format-candidate results)))
candidates)))
;;;###autoload
(defun helm-lean-definitions ()
"Open a 'helm' interface for searching Lean definitions."
(interactive)
(require 'helm)
(helm :sources (helm-build-sync-source "helm-source-lean-definitions"
:requires-pattern 1
:candidates 'helm-lean-definitions-candidates
:volatile t
:match 'identity
:action '(("Go to" . (lambda (c) (with-helm-current-buffer
(apply 'lean-find-definition-cont (plist-get c :source)))))))
:buffer "*helm Lean definitions*"))
;;;###autoload
(defun helm-lean-hook ()
"Set up helm-lean for current buffer"
(local-set-key helm-lean-keybinding-helm-lean-definitions #'helm-lean-definitions))
;;;###autoload
(add-hook 'lean-mode-hook #'helm-lean-hook)
(provide 'helm-lean)
;;; helm-lean.el ends here