michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(emacs): add shortcut for using --hott option

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-29 10:57:52 -07:00
parent 793b2817ec
commit c0039735f4
1 changed files with 15 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/emacs/lean-mode.el
View file

@ -9,16 +9,25 @@
(defun flymake-create-temp-lean-in-system-tempdir (filename prefix)
(make-temp-file (or prefix "flymake") nil ".lean"))
(defun lean-execute ()
(defun lean-execute (&optional arg)
"Execute Lean in the current buffer"
(interactive)
(interactive "sarg: ")
(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)))))
(compile (format "%s %s %s" lean-exe (if arg arg "") (buffer-file-name)))
(compile (format "%s $s %s" lean-exe (if arg arg "") (flymake-init-create-temp-buffer-copy) 'flymake-create-temp-lean-in-system-tempdir))))
(defun lean-std-exe ()
(interactive)
(lean-execute))
(defun lean-hott-exe ()
(interactive)
(lean-execute "--hott"))
(defun lean-set-keys ()
(local-set-key "\C-c\C-x" 'lean-execute)
(local-set-key "\C-c\C-l" 'lean-execute))
(local-set-key "\C-c\C-x" 'lean-std-exe)
(local-set-key "\C-c\C-l" 'lean-std-exe)
(local-set-key "\C-c\C-k" 'lean-hott-exe))
(define-abbrev-table 'lean-mode-abbrev-table '(
("var" "variable")