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

feat(emacs/lean-project): add lean-project-create to imenu

Browse source 
Related with #170
This commit is contained in:
Soonho Kong 2014-09-10 15:18:26 -07:00
parent b05ca1db0f
commit 1c5497e632
2 changed files with 42 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -26,6 +26,7 @@
(require 'lean-mmm-lua) (require 'lean-mmm-lua)
(require 'lean-company) (require 'lean-company)
(require 'lean-server) (require 'lean-server)
(require 'lean-project)
(defun lean-compile-string (exe-name args file-name) (defun lean-compile-string (exe-name args file-name)
"Concatenate exe-name, args, and file-name" "Concatenate exe-name, args, and file-name"
@ -93,6 +94,7 @@
"Menu for the Lean major mode" "Menu for the Lean major mode"
`("Lean" `("Lean"
["Execute lean" lean-execute t] ["Execute lean" lean-execute t]
["Create a new project" (call-interactively 'lean-project-create) (not (lean-project-inside-p))]
"-----------------" "-----------------"
["Show type info" lean-eldoc-documentation-function lean-eldoc-use] ["Show type info" lean-eldoc-documentation-function lean-eldoc-use]
["Fill a placeholder" lean-fill-placeholder (looking-at (rx symbol-start "_"))] ["Fill a placeholder" lean-fill-placeholder (looking-at (rx symbol-start "_"))]

40
src/emacs/lean-project.el Normal file
View file

@ -0,0 +1,40 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'flycheck)
(require 'lean-util)
(defconst lean-project-file-name ".project"
"Project file name")
(defun lean-project-find-root ()
(lean-find-file-upward lean-project-file-name))
(defun lean-project-inside-p ()
(if (lean-project-find-root) t nil))
(defun lean-project-create (directory)
(interactive
(list (read-directory-name "Project root: ")))
(let ((project-file (concat (file-name-as-directory directory)
lean-project-file-name)))
(if (file-exists-p project-file)
(user-error "project-file %s already exists" project-file))
(find-file project-file)
(insert (string-join '("# Lean project file"
""
"# Include all .lean files under this directory"
"+ *.lean"
""
"# Exclude flycheck generated temp files"
"- flycheck*.lean"
""
"# Exclude emacs temp files"
"- .#*.lean")
"\n"))
(save-buffer)))
(provide 'lean-project)