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

feat(emacs/lean-project.el): ask 'project type' in lean-project-create

Browse source 
close #999
This commit is contained in:
Soonho Kong 2016-02-12 22:02:24 -05:00
parent b047c9c037
commit ca1901bb2c
1 changed files with 21 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/emacs/lean-project.el
View file

@ -16,25 +16,32 @@
(defun lean-project-inside-p ()
(if (lean-project-find-root) t nil))
(defun lean-project-create (directory)
(defun lean-project-create (directory type)
(interactive
(list (read-directory-name "Specify the project root directory: ")))
(list (read-directory-name "Specify the project root directory: ")
(intern (completing-read "Project type:: " '(standard hott)))))
(let ((project-file (concat (file-name-as-directory directory)
lean-project-file-name)))
lean-project-file-name))
(ext (pcase type
(`standard "lean")
(`hott "hlean")))
(default-contents
(s-join "\n"
;; EXT is a placeholder.
'("# Lean project file"
""
"# Include all .EXT files under this directory"
"+ *.EXT"
""
"# Exclude flycheck generated temp files"
"- flycheck*.EXT"
""
"# Exclude emacs temp files"
"- .#*.EXT"))))
(if (file-exists-p project-file)
(user-error "project-file %s already exists" project-file))
(find-file project-file)
(insert (s-join "\n"
'("# Lean project file"
""
"# Include all .lean files under this directory"
"+ *.lean"
""
"# Exclude flycheck generated temp files"
"- flycheck*.lean"
""
"# Exclude emacs temp files"
"- .#*.lean")))
(insert (s-replace "EXT" ext default-contents))
(save-buffer)))
(provide 'lean-project)