From bc0a8b8da43a88cc39d09a39fd10e1f082a886ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 27 Jul 2014 17:03:06 -0700 Subject: [PATCH] feat(emacs): make lean-mode org-mode friendly Signed-off-by: Leonardo de Moura --- src/emacs/lean-mode.el | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 04cf3b8778..c82f298bc8 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -1,14 +1,20 @@ (require 'generic-x) (require 'lean-input) (require 'compile) +(require 'flymake) (defvar lean-exe "lean" "Path for the Lean executable") +(defun flymake-create-temp-lean-in-system-tempdir (filename prefix) + (make-temp-file (or prefix "flymake") nil ".lean")) + (defun lean-execute () "Execute Lean in the current buffer" (interactive) - (compile (format "%s %s" lean-exe (buffer-file-name)))) + (if (buffer-file-name) + (compile (format "%s %s" lean-exe (buffer-file-name))) + (compile (format "%s %s" lean-exe (flymake-init-create-temp-buffer-copy 'flymake-create-temp-lean-in-system-tempdir))))) (defun lean-set-keys () (local-set-key "\C-c\C-x" 'lean-execute)