From 7a1ee92507dcd763c44fc2d4d080a115cfb0b6a2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Jan 2014 11:45:31 -0800 Subject: [PATCH] feat(emacs): add short-cuts \C-c\C-l and \C-c\C-x to execute Lean files in Emacs Signed-off-by: Leonardo de Moura --- emacs/lean-mode.el | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/emacs/lean-mode.el b/emacs/lean-mode.el index e95eb272f..8c6b20460 100644 --- a/emacs/lean-mode.el +++ b/emacs/lean-mode.el @@ -1,5 +1,18 @@ (require 'generic-x) (require 'lean-input) +(require 'compile) + +(defvar lean-exe "lean" + "Path for the Lean executable") + +(defun lean-execute () + "Execute Lean in the current buffer" + (interactive) + (compile (format "%s %s" lean-exe (buffer-file-name)))) + +(defun lean-set-keys () + (local-set-key "\C-c\C-x" 'lean-execute) + (local-set-key "\C-c\C-l" 'lean-execute)) (define-generic-mode 'lean-mode ;; name of the mode to create @@ -14,6 +27,7 @@ (set-input-method "Lean") (set (make-local-variable 'lisp-indent-function) 'common-lisp-indent-function) + (lean-set-keys) )) "A mode for Lean files" ;; doc string for this mode )